2 citations · 2 across the 2 of their papers we have counts for
3 papers
cs.LO2022★ 2 cited
Realizability Checking of Contracts with Kind 2
Daniel Larraz, Cesare Tinelli
We present a new feature of the open-source model checker Kind 2 which checks whether a component contract is realizable; i.e., it is possible to construct a component such that fo…
cs.LO2021
Merit and Blame Assignment with Kind 2
Daniel Larraz, Mickaël Laurent, Cesare Tinelli
We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, gu…
cs.LO2020
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
Cristina Borralleras, Daniel Larraz, Albert Oliveras +2
We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists in decid…