Concept
Satisfiability modulo theories
Publications associées (73)
The Complexity of Satisfiability Checking for Symbolic Finite Automata
We study the satisfiability problem of symbolic finite automata and decompose it into the satisfiability problem of the theory of the input characters and the monadic second-order theory of the indices of accepted words. We use our decomposition to obtain ...
2023NP 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, Cham2022On Proving and Disproving Equivalence of Functional Programming Assignments
Viktor Kuncak, Dragana Milovancevic
We present an automated approach for verifying the correctness of programming assignments, such as ones arising in a functional programming course. Our approach takes a small set of reference implementations and a set of student implementations and checks, ...
2021Consolidation of database check constraints
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 ...
2019Refutation-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