Browse Proceedings

The Coccinelle system is a program transformer used to automate and document collateral evolutions in Linux device drivers. Semantics are developed for the its underlying semantic patch language (SmPL). A richer and more efficient version is defined, ...

The security of a software system is almost always retrofitted to an afterthought. When security problems arise, understanding and correcting them can be very challenging. On the one hand, the programanalysis and programming-languages research community ...

Integer octagonal constraints (a.k.a. Unit Two Variables Per Inequality or UTVPI integer constraints) constitute an interesting class of constraints for the representation and solution of integer problems in the fields of constraint programming and ...

We consider verification of safety properties for parameterized systems with linear topologies. A process in the system is an extended automaton, where the transitions are guarded by both local and global conditions. The global conditions are non-atomic,...

We define an abstraction of the continuous variables that serve as inputs to embedded software. In existing static analyzers, these variables are most often abstracted by a constant interval, and this approach has shown its limits. We propose a ...

Realizability - checking whether a specification can be implemented by an open system - is a fundamental step in the design flow. However, if the specification turns out not to be realizable, there is no method to pinpoint the causes for ...

Model checking using Craig interpolants provides an effective method for computing an over-approximation of the set of reachable states using a SAT solver. This method requires proofs of unsatisfiability from the SAT solver to progress. If an over-...

Cellular signalling pathways, where proteins can form complexes and undergo a large array of post translational modifications are highly combinatorial systems sending and receiving extracellular signals and triggering appropriate responses. Process-...

Lazy abstraction builds up an abstract reachability tree by locally refining abstractions in order to eliminate spurious counterexamples in smaller and smaller subtrees. The method has proven useful to verify systems code. It is still open how good the ...

We endow action sets of transition systems with a partial order that expresses the degree of specialization of actions, and with an intuitive but flexible consistency predicate that constrains the extension of such orders with more specialized actions. ...

Simulation and formal verification are two complementary techniques for checking the correctness of hardware and software designs. Formal verification proves that a design property holds for all points of the search space while simulation checks this ...

In model-driven verification a model checker executes a program by embedding it within a test harness, thus admitting program verification without the need to translate the program, which runs as native code. Model checking techniques in which code is ...

In this paper we analyze the problem of transforming partitions in order to satisfy completeness in the standard abstract interpretation framework. In order to obtain this, we exploit the relation existing between completeness and the Paige-Tarjan ...

Finding useful sharing information between instances in object-oriented programs has recently been the focus of much research. The applications of such static analysis are multiple: by knowing which variables definitely do not share in memory we can ...

Assertion checking is the restriction of program verification to validity of program assertions. It encompasses safety checking, which is program verification of safety properties, like memory safety or absence of overflows. In this paper, we consider ...

Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications ...

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting ...

The paper presents a new deductive rule for verifying response properties under the assumption of compassion (strong fairness) requirements. It improves on previous rules in that the premises of the new rule are all first order.We prove that the rule is ...

Abstraction refinement-based model checking has become a standard approach for efficiently verifying safety properties of hardware/software systems. Abstraction refinement algorithms can be guided by counterexamples generated from abstract transition ...

We show that every abstract interpretation possesses an internal logic, whose proof theory is defined by the partial ordering on the abstract domain's elements and whose model theory is defined by the domain's concretization function. We explain how ...

Temporal logics like LTL are frequently used for the specification and verification of reactive systems. For verification, LTL formulas are typically translated to generalized nondeterministic Büchi automata so that the verification problem is reduced ...

We present highly accurate deterministic and randomized methods for monitoring temporal properties of stochastic systems. The deterministic algorithms employ timeouts that are set dynamically to achieve desired accuracy. The randomized algorithms employ ...

In the game theoretic approach to the synthesis of reactive systems, specifications are often given in linear time logic (LTL). Computing a winning strategy to an infinite game whose winning condition is the set of LTL properties is the main step in ...