08:30 - 09:00

• Efficient Scalable Verification of LTL Specifications

  Linear Temporal Logic (LTL) has been used in computer science for decades to formally specify programs, systems, desired properties, and relevant behaviors. This paper presents a novel, efficient technique for verifying LTL specifications in a fully automated way. Our technique belongs to the category of Bounded Satisfiability Checking approaches, where LTL formulae are encoded as formulae of another decidable logic that can be solved through modern satisfiability solvers. The target logic in our approach is Bit-Vector Logic. We present our novel encoding, show its correctness, and experimentally compare it against existing encodings implemented in well-known formal verification tools.

Luciano Baresi; Mohammad Mehdi Pourhashem Kallehbasti; Matteo Rossi

Politecnico di Milano, Italy

09:00 - 09:30

• Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification

  Formal verification can provide the highest degree of software assurance. Demand for it is growing, but there are still few projects that have successfully applied it to sizeable, real-world systems. This lack of experience makes it hard to predict the size, effort and duration of verification projects. In this paper, we aim to better understand possible leading indicators of proof size. We present an empirical analysis of proofs from the landmark formal verification of the seL4 microkernel and the two largest software verification proof developments in the Archive of Formal Proofs. Together, these comprise 15,018 individual lemmas and approximately 215,000 lines of proof script. We find a consistent quadratic relationship between the size of the formal statement of a property, and the final size of its formal proof in the interactive theorem prover Isabelle. Combined with our prior work, which has indicated that there is a strong linear relationship between proof effort and proof size, these results pave the way for effort estimation models to support the management of large-scale formal verification projects.

   

  Preprint available:

Daniel Matichuk; Toby Murray; June Andronick; Ross Jeffery; Gerwin Klein; Mark Staples

NICTA, Australia; University of New South Wales, Australia

09:30 - 10:00

• Specifying Event-Based Systems with a Counting Fluent Temporal Logic

  Fluent linear temporal logic is a formalism for specifying properties of event-based systems, based on propositions called fluents, defined in terms of activating and deactivating events. In this paper, we propose complementing the notion of fluent by the related concept of counting fluent. As opposed to the boolean nature of fluents, counting fluents are numerical values, that enumerate event occurrences, and allow us to specify naturally some properties of reactive systems. Although by extending fluent linear temporal logic with counting fluents we obtain an undecidable, strictly more expressive formalism, we develop a sound (but incomplete) model checking approach for the logic, that reduces to traditional temporal logic model checking, and allows us to automatically analyse properties involving counting fluents, on finite event-based systems. Our experiments, based on relevant models taken from the literature, show that: (i) counting fluent temporal logic is better suited than traditional temporal logic for expressing properties in which the number of occurrences of certain events is relevant, and (ii) our model checking approach on counting fluent specifications has an efficiency that is comparable to that of model checking equivalent fluent temporal logic specifications, while our approach scales better.

   

  Preprint available:

Germán Regis; Renzo Degiovanni; Nicolás D'Ippolito; Nazareno Aguirre

Universidad Nacional de Río Cuarto, Argentina; Universidad de Buenos Aires, Argentina

10:00 - 10:30

• Coexecutability for Efficient Verification of Data Model Updates

  Modern applications use back-end data stores for persistent data. Automated verification of the code that updates the data store would prevent bugs that can cause loss or corruption of data. In this paper, we focus on the most challenging part of this problem: automated verification of code that updates the data store and contains loops. Due to dependencies between loop iterations, verification of code that contains loops is a hard problem, and typically requires manual assistance in the form of loop invariants. We present a fully automated technique that improves verifiability of loops. We first define co execution, a method for modeling loop iterations that simplifies automated reasoning about loops. Then, we present a fully automated static program analysis that detects whether the behavior of a given loop can be modeled using co execution. We provide a customized verification technique for co executable loops that results in more effective verification. In our experiments we observed that, in 45% of cases, modeling loops using co execution reduces verification time between 1 and 4 orders of magnitude. In addition, the rate of inconclusive verification results in the presence of loops is reduced from 65% down to 24%, all without requiring loop invariants or any manual intervention.

   

  Preprint available:

Ivan Bocic; Tevfik Bultan

University of California at Santa Barbara, USA