Publication
On Combining Theories with Shared Set Operations
Related publications (35)
Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization
Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very
many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy
various constraints. In this thesis, we demonstrate how for ...
EPFL2018Canonical Computation without Canonical Representation
Mathias Soeken, Luca Gaetano Amarù, Ana Petkovska
A representation of a Boolean function is canonical if, given a variable order, only one instance of the representation is possible for the function. A computation is canonical if the result depends only on the Boolean function and a variable order, and do ...
IEEE2018Busy Man’s Synthesis: Combinational Delay Optimization With SAT
Giovanni De Micheli, Mathias Soeken
Boolean SAT solving can be used to find a minimum- size logic network for a given small Boolean function. This paper extends the SAT formulation to find a minimum-size network under delay constraints. Delay constraints are given in terms of input arrival t ...
Ieee2017metaSMT: focus on your application and not on solver integration
Many applications from artificial intelligence and formal methods use decision procedures as their core solving engines. In this context, automated reasoning based on Satisfiability (SAT) or Satisfiability Modulo Theories (SMT) is very effective. For a giv ...
Springer Verlag2017Solving quantified linear arithmetic by counterexample-guided instantiation
Viktor Kuncak, Andrew Joseph Reynolds
This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...
2017On 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 ...
2016Atomic distributions in crystal structures solved by Boolean satisfiability techniques
The atomic distribution in crystal structures becomes very complex if atoms are disordered and randomly distributed over positions not being fully occupied. Interatomic distances between neighboring atoms might be too close for simultaneous occupancies and ...
2016Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications
Giovanni De Micheli, Paolo Ienne, Mathias Soeken, Ana Petkovska
Lexicographic Boolean satisfiability (LEXSAT) is a variation of the Boolean satisfiability problem (SAT). Given a variable order, LEXSAT finds a satisfying assignment whose integer value under the given variable order is minimum (maximum) among all satisfi ...
Assoc Computing Machinery2016A 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