Publication
Solving quantified linear arithmetic by counterexample-guided instantiation
Publications associées (33)
Interpolation and Quantifiers in Ortholattices
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...
2024Interpolation and Quantifiers in Ortholattices
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...
Cham2024Decision Procedures for Power Structures
We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...
EPFL2023NP Satisfiability for Arrays as Powers
We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...
Springer, Cham2022Scaling Language Features for Program Verification
Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
EPFL2022Complexity of linear relaxations in integer programming
For a set X of integer points in a polyhedron, the smallest number of facets of any polyhedron whose set of integer points coincides with X is called the relaxation complexity rc(X). This parameter was introduced by Kaibel & Weltge (2015) and captures the ...
2020Verified Functional Programming
In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language.
Our system is based on a dependently-typed language and an algorithmic type checking procedure
which ensures total correctness. We rely on SMT solve ...
EPFL2019On Satisfiability for Quantified Formulas in Instantiation-Based Procedures
Viktor Kuncak, Nicolas Charles Yves Voirol
Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...
2016Automating Verification of Functional Programs with Quantified Invariants
Viktor Kuncak, Nicolas Charles Yves Voirol
We present the foundations of a verifier for higher-order functional programs with generics and recursive algebraic data types. Our ver- ifier supports finding sound proofs and counterexamples even in the presence of certain quantified invariants and recur ...
2016A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...
Springer-Verlag Berlin2015