Publication
Solving quantified linear arithmetic by counterexample-guided instantiation
Related publications (33)
Comfusy: A Tool for Complete Functional Synthesis
Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesi ...
Springer2010On Complete Reasoning about Axiomatic Specifications
Automated software verification tools typically accept specifications of functions in terms of pre- and postconditions. However, many properties of functional programs can be more naturally specified using a more general form of universally quantified prop ...
2010Combining Theories with Shared Set Operations
Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...
Springer2009On Combining Theories with Shared Set Operations
We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...
2009Finding 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 Usa2009Decision Procedures for Multisets with Cardinality Constraints
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 c ...
Springer2008Non-Clausal Satisfiability Modulo Theories
This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is resp ...
2008Linear Arithmetic with Stars
We consider an extension of integer linear arithmetic with a “star” operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We show that the satisfiability problem for this extended language remains in NP (and th ...
Springer2008On Linear Arithmetic with Stars
We consider an extension of integer linear arithmetic with a star operator that takes closure under vector addition of the set of solutions of linear arithmetic subformula. We show that the satisfiability problem for this language is in NP (and therefore N ...
2008Formal semantics for refinement verification of entreprise models
In this dissertation we investigate how Business/IT alignment in enterprise models can be enhanced by using a software engineering stepwise refinement paradigm. To have an IT system that supports an enterprise and meets the enterprise business needs, manag ...
EPFL2008