Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userVerifying Correct Usage of Context-Free API Protocols (Extended Version)
85
0
0.0
(
0
)
Added by
Kostas Ferles
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Several real-world libraries (e.g., reentrant locks, GUI frameworks, serialization libraries) require their clients to use the provided API in a manner that conforms to a context-free specification. Motivated by this observation, this paper describes a new technique for verifying the correct usage of context-free API protocols. The key idea underlying our technique is to over-approximate the programs feasible API call sequences using a context-free grammar (CFG) and then check language inclusion between this grammar and the specification. However, since this inclusion check may fail due to imprecision in the programs CFG abstraction, we propose a novel refinement technique to progressively improve the CFG. In particular, our method obtains counterexamples from CFG inclusion queries and uses them to introduce new non-terminals and productions to the grammar while still over-approximating the programs relevant behavior. We have implemented the proposed algorithm in a tool called CFPChecker and evaluate it on 10 popular Java applications that use at least one API with a context-free specification. Our evaluation shows that CFPChecker is able to verify correct usage of the API in clients that use it correctly and produces counterexamples for those that do not. We also compare our method against three relevant baselines and demonstrate that CFPChecker enables verification of safety properties that are beyond the reach of existing tools.
rate research
Read More
The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and context-free properties by ensuring decidability and tractability in the combined setting. To this end we introduce two real-time linear temporal logics for specifying quantitative timing context-free requirements in a pointwise semantics setting: Event-Clock Nested Temporal Logic (ECNTL) and Nested Metric Temporal Logic (NMTL). The logic ECNTL is an extension of both the logic CARET (a context-free extension of standard LTL) and Event-Clock Temporal Logic (a tractable real-time logical framework related to the class of Event-Clock automata). We prove that satisfiability of ECNTL and visibly model-checking of Visibly Pushdown Timed Automata VPTA against ECNTL are decidable and EXPTIME-complete. The other proposed logic NMTL is a context-free extension of standard Metric Temporal Logic (MTL). It is well known that satisfiability of future MTL is undecidable when interpreted over infinite timed words but decidable over finite timed words. On the other hand, we show that by augmenting future MTL with future context-free temporal operators, the satisfiability problem turns out to be undecidable also for finite timed words. On the positive side, we devise a meaningful and decidable fragment of the logic NMTL which is expressively equivalent to ECNTL and for which satisfiability and visibly model-checking of VPTA are EXPTIME-complete.
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, and is often neglected in the metatheory of gradual languages. In this paper, we propose an axiomatic account of program equivalence in a gradual cast calculus, which we formalize in a logic we call gradual type theory (GTT). Based on Levys call-by-push-value, GTT gives an axiomatic account of both call-by-value and call-by-name gradual languages. We then prove theorems that justify optimizations and refactorings in gradually typed languages. For example, uniqueness principles for gradual type connectives show that if the $betaeta$ laws hold for a connective, then casts between that connective must be equivalent to the lazy cast semantics. Contrapositively, this shows that eager cast semantics violates the extensionality of function types. As another example, we show that gradual upcasts are pure and dually, gradual downcasts are strict. We show the consistency and applicability of our theory by proving that an implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parametrized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.
Nowadays, developers often reuse existing APIs to implement their programming tasks. A lot of API usage patterns are mined to help developers learn API usage rules. However, there are still many missing variables to be synthesized when developers integrate the patterns into their programming context. To deal with this issue, we propose a comprehensive approach to integrate API usage patterns in this paper. We first perform an empirical study by analyzing how API usage patterns are integrated in real-world projects. We find the expressions for variable synthesis is often non-trivial and can be divided into 5 syntax types. Based on the observation, we promote an approach to help developers interactively complete API usage patterns. Compared to the existing code completion techniques, our approach can recommend infrequent expressions accompanied with their real-world usage examples according to the user intent. The evaluation shows that our approach could assist users to integrate APIs more efficiently and complete the programming tasks faster than existing works.
We present an imperative object calculus where types are annotated with qualifiers for aliasing and mutation control. There are two key novelties with respect to similar proposals. First, the type system is very expressive. Notably, it adopts the recovery approach, that is, using the type context to justify strengthening types, greatly improving its power by permitting to recover uniqueness and immutability properties even in presence of other references. This is achieved by rules which restrict the use of such other references in the portion of code which is recovered. Second, execution is modeled by a non standard operational model, where properties of qualifiers can be directly expressed on source terms, rather than as invariants on an auxiliary structure which mimics physical memory. Formally, this is achieved by the block construct, introducing local variable declarations, which, when evaluated, play the role of store.
Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called $epsilon$-robustness, which characterizes possible distance between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noi
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
