Publication
Automated Formal Verification of Software Network Functions
Related publications (42)
Programming with Specifications
This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...
EPFL2012Decision Procedures for Program Synthesis and Verification
Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...
EPFL2011StagedSAC: a case study in performance-oriented DSL development
Martin Odersky, Tiark Rompf, Vlad Ureche, Hassan Chafi
Domain-specific languages (DSLs) can bridge the gap between high-level programming and efficient execution. However, implementing compiler tool-chains for performance oriented DSLs requires significant effort. Recent research has produced methodologies and ...
ACM2011On Satisfiability Modulo Computable Functions
Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal
We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...
2010Software Verification by Combining Program Analyses of Adjustable Precision
In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...
EPFL2010Shape Refinement through Explicit Heap Analysis
Dirk Thilo Beyer, Grégory Théoduloz, Damien Zufferey
Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structu ...
Springer2010Automatic Verification of Parametric Specifications with Complex Topologies
The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple ve ...
2010Compiling generics through user-directed type specialization
Compilation of polymorphic code through type erasure gives compact code but performance on primitive types is significantly hurt. Full specialization gives good performance, but at the cost of increased code size and compilation time. Instead we propose a ...
ACM2009Finding Loop Invariants for Programs over Arrays Using a Theorem Prover
We present a new method for automatic generation of loop invariants for programs containing arrays. Unlike all previously known methods, our method allows one to generate first-order invariants containing alternations of quantifiers. The method is based on ...
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2009Full Functional Verification of Linked Data Structures
We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify form ...
2008