VERIFY on Tuesday, August 15th

Session 1 (09:00‑10:00)

09:00‑10:00

John Rushby (SRI International) Threatened by a Great Opportunity: Disruptive Innovation in Formal Verification [pdf] Low-end disruptive innovation occurs when a technology, aimed at customers who do not require the full performance of the incumbent high-end technology, maintains a rapid rate of improvement and eventually overhauls and displaces the incumbent. Examples are the microprocessor (vs. mainframes) and digital (vs. film) photography. In formal verification, the examples are model checking and static analysis and related methods in relation to interactive theorem proving. I will describe one disruptive technology--SMT Solvers and their application to bounded model checking and k-induction for infinite state systems--in some detail and will demonstrate how verifications that used to take weeks to develop and hours to run are now reduced to hours and seconds, respectively, and are completely automated. Developers and users of high-end verification systems may regard this disruption as a threat, but I will argue that it is better seen as an opportunity and will propose an "evidential tool bus" architecture that allows these technologies to coexist so that the power of the whole is greater than any of its components.

Break (10:00‑10:30)

Session 2: Verification Tools I (10:30‑12:00)

10:30‑11:00	Myla Archer (Naval Research Laboratory) Elizabeth Leonard (Naval Research Laboratory) Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode Using a theorem prover to establish that a body of code correctly implements an algorithm is a task seldom undertaken because the effort required tends to be prohibitive. Direct reasoning about code in a particular programming language requires that some version of the language's semantics---e.g., axiomatic, operational, denotational---be used to determine the program correctness assertions to establish with the theorem prover. Any scheme for generating correctness assertions will be language-specific, and for languages with complex constructs, can be complex to implement and use. Direct reasoning about algorithms using a theorem prover can be not just difficult, but impossible, if the algorithms are (as is typical) specified using informal pseudocode. This paper outlines a scheme that falls short of full program verification yet provides high confidence in the correctness of an algorithm's implementation. The scheme uses formal pseudocode specifications, in a restricted language of while programs with (possibly recursive) procedure calls, to bridge from algorithm specifications to implementations in code. Each block of formal pseudocode is verified in the theorem prover PVS by translating it into a state machine model and proving a set of state invariants. High confidence in implementation correctness is achieved by combining verification of the pseudocode with traceability arguments relating the algorithm specification to the pseudocode representation and the pseudocode representation to the actual code.
11:00‑11:30	Robert Palmer (The University of Utah, School of Computing) Ganesh Gopalakrishnan (University of Utah) Mike Kirby (Univ of Utah) Formal Specification and Verification Using +CAL: An Experience Report We present a case study on the use of the +CAL specification language as applied to the process interaction semantics of the MPI standard. We also present preliminary, but highly encouraging, results from a generalization of the notion of cluster-based partial-order reduction in the context of +CAL model checking. Called generalized static reduction (GSR), this approach takes advantage of the commuting nature of many MPI send/receive operation types. Preliminary results confirm that +CAL is a user-friendly and less error-prone notation than TLA+ (into which +CAL compiles), and syntactically supports the kind of transition annotations that GSR requires. Our preliminary evaluation of GSR on a simple example shows that with it, TLC (the TLA+ model checker) can handle a 128-process model in 8 hours, when all conceivable alternatives on this example will not finish their state enumeration.
11:30‑12:00	Bernhard Beckert (University of Koblenz) Vladimir Klebanov (University of Koblenz) Must Program Verification Systems and Calculi be Verified? With this paper, we want to provoke discussion on whether verification tools and calculi themselves need to be formally verified. We argue that though verifying the verifier is useful, it is not an absolute necessity. The (limited) resources in academia may be better spent on improving verification systems in other ways.

Lunch break (12:30‑14:00)

Session 3: Verification Tools II (14:00‑15:30)

14:00‑14:30	Sara Van Langenhove (Ghent University) Albert Hoogewijs (Ghent University) Verifying Sliced Hierarchical Statecharts with SVtL To successfully produce correct UML software systems, the way the software development process is handled is an essential ingredient. The SVtL (System Verification through Logic) framework is the core of a slicing-based verification environment for improving the quality of systems whose behavior is designed using UML statecharts. The framework is designed in such a way that the analyst only needs knowledge of UML and the system studied. In the current paper, we present an overview of the SVtL software architecture together with some design decisions and stress the strength of the underlying slicing-based formal methodology.
14:30‑15:00	Laura Ildiko Kovacs (Research Institute for Symbolic Computation, Linz) Tudor Jebelean (Research Institute for Symbolic Computation, Linz) Finding Polynomial Invariants for Imperative Loops in the Theorema System We present an algorithm for finding valid polynomial relations (i.e. invariants) among program variables for imperative loops. The algorithm is implemented in the verification environment for imperative programs (using Hoare logic) in the frame of the Theorema system (www.theorema.org). The algorithm uses techniques from (polynomial) algebra and combinatorics, namely Groebner Bases, variable elimination, algebraic dependencies and symbolic summation (the Gosper algorithm, handling geometric series, C-finite solving). These methods are demonstrated on several examples which have been treated automatically by our implementation.
15:00‑15:30	Achim D. Brucker (ETH Zürich) Burkhart Wolff (ETH Zurich) A Package for Extensible Object-Oriented Data Models with an Application to IMP++ We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, and accessors functions, coercions between dynamic and static types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for a object-oriented core-language called IMP++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven.

Break (15:30‑16:00)

Session 4: Information Flow Security (16:00‑17:00)

16:00‑16:30

Raghavendra Kagalavadi Ramesh (Indian Institute of Science, Bangalore) Deepak D'Souza (Indian Institute of Science, Bangalore) Checking Unwinding Conditions for Finite State Systems We consider the problem of checking the unwinding conditions of Mantel for Basic Security Predicates (BSP's) \cite{Mantel:2003}, for finite-state systems. We show how the unwinding conditions can be simplified to checking conditions on a maximal simulation relation. We conclude that the time complexity of verifying BSP's via the unwinding route compares favourably with the model-checking technique proposed in \cite{ARSPA:D'Souza/R/Sprick:2005}

16:30‑17:00

Dieter Hutter (DFKI) Automating Proofs of Unwinding Conditions In previous work we illustrated how information flow control techniques can be used to specify and verify security requirements of multi-agent systems by decomposing them to requirements of individual agents. While we illustrated how security requirements of an overall multi-agent system can be decomposed to requirements of individual agents, there was still the problem of how to automate the verification of the resulting proof obligations. In this paper we present heuristics to guide an tactical (inductive) theorem prover when searching for such proofs. Our approach is based on Mantel's MAKS framework on possibilistic information flow control to formulate security predicates.