Publications related to Satisfiability modulo theories

NP 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, Cham2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

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 ...

EPFL2022

Proving and Disproving Equivalence of Functional Programming Assignments

Viktor Kuncak, Dragana Milovancevic

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

2023

Consolidation of database check constraints

Nikola Obrenovic

Independent modeling of various modules of an information system (IS), and consequently database subschemas, may result in formal or semantic conflicts between the modules being modeled. Such conflicts may cause collisions between the integrated database s ...

2019

Refutation-based synthesis in SMT

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

SPRINGER2019

Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization

Andrew James Becker

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 ...

EPFL2018

Canonical 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 ...

IEEE2018

Generating Safety Guidance for Medical Injection with Three-Compartment Pharmacokinetics Model

Giovanni De Micheli, Francesca Stradolini, Heinz Riener, Cunxi Yu

Medical cyber-physical systems are a new trend of software controlled physical systems that are increasingly common in medical domains. With rapid developments in medical science and computer technology, safety verification and simulation becomes more chal ...

IEEE2018

A Framework for the Secretary Problem on the Intersection of Matroids

Ola Nils Anders Svensson, Moran Feldman, Rico Zenklusen

The secretary problem became one of the most prominent online selection problems due to its numerous applications in online mechanism design. The task is to select a maximum weight subset of elements subject to given constraints, where elements arrive one- ...

ASSOC COMPUTING MACHINERY2018

Practical Exact Synthesis

Giovanni De Micheli, Mathias Soeken, Luca Gaetano Amarù, Eleonora Testa, Winston Jason Haaswijk

In this paper, we discuss recent advances in exact synthesis, considering both their efficient implementation and various applications in which they can he employed. We emphasize on solving exact synthesis through Boolean satisfiability (SAT) encodings. Di ...

IEEE2018

Exact Synthesis of Majority-Inverter Graphs and Its Applications

Giovanni De Micheli, Mathias Soeken, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

We propose effective algorithms for exact synthesis of Boolean logic networks using satisfiability modulo theories (SMT) solvers. Since exact synthesis is a difficult problem, it can only be applied efficiently to very small functions, having up to 6 varia ...

Ieee-Inst Electrical Electronics Engineers Inc2017

Constraint-Flow Nets: A Model for Building Constraints from Resource Dependencies

Simon Bliudze, Alena Simalatsar, Alina Zolotukhina

The major research in the resource management literature focuses primarily on two complementary sub-problems: (1) specification languages for formulating resource requests and (2) constraint problems modelling allocation and scheduling. Both directions ass ...

Springer International Publishing2017

Solving 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 ...

2017

Busy 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 ...

Ieee2017

Exploiting Satisfiability Solvers for Efficient Logic Synthesis

Ana Petkovska

Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...

EPFL2017

Optimizing Majority-Inverter Graphs with Functional Hashing

Giovanni De Micheli, Mathias Soeken, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

A Majority-Inverter Graph (MIG) is a recently introduced logic representation form whose algebraic and Boolean properties allow for efficient logic optimization. In particular, when considering logic depth reduction, MIG algorithms obtained signific ...

IEEE2016

Fast 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 Machinery2016

SMT-Based Checking of Predicate-Qualified Types for Scala

Viktor Kuncak, Georg Stefan Schmid

We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in ...

Assoc Computing Machinery2016

A Sound and Complete Axiomatization of Majority-n Logic

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù, Anupam Chattopadhyay

Manipulating logic functions via majority operators recently drew the attention of researchers in computer science. For example, circuit optimization based on majority operators enables superior results as compared to traditional logic systems. Also, the B ...

Institute of Electrical and Electronics Engineers2016

Exploiting Inherent Characteristic of Reversible Circuits for Faster Combinational Equivalence Checking

Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon, Luca Gaetano Amarù

Reversible circuits implement invertible logic functions. They are of great interest to cryptography, coding theory, interconnect design, computer graphics, quantum computing, and many other fields. As for conventional circuits, checking the combinational ...

Ieee2016