265 citations
- Institut national de recherche en sciences et technologies du numériqueFR22 papers
- Geometric (India)IN8 papers
- Institut de Mathématiques de BordeauxFR8 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR8 papers
- Centre Inria de l'université de BordeauxFR7 papers
- Centre Inria de l'Université de LorraineFR5 papers
- Centre National de la Recherche ScientifiqueFR5 papers
- Laboratoire Bordelais de Recherche en InformatiqueFR5 papers
- Université de LorraineFR5 papers
- Graz University of TechnologyAT4 papers
- Nantes UniversitéFR4 papers
- École PolytechniqueFR3 papers
6 papers · 1 filter
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Martin Bromberger, Irina Dragoste, Rasha Faqeh +6
In a previous paper, we have shown that clause sets belonging to the Horn Bernays-Schönfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clau…
E-Cyclist: Implementation of an Efficient Validation of FOLID Cyclic Induction Reasoning
Sorin Stratulat
Checking the soundness of cyclic induction reasoning for first-order logic with inductive definitions (FOLID) is decidable but the standard checking method is based on an exponenti…
Alethe: Towards a Generic SMT Proof Format (extended abstract)
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa +1
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are use…
A Benchmarks Library for Extended Parametric Timed Automata
Étienne André, Dylan Marinho, Jaco van de Pol
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new…
The Challenge of Unifying Semantic and Syntactic Inference Restrictions
Christoph Weidenbach
While syntactic inference restrictions don't play an important role for SAT, they are an essential reasoning technique for more expressive logics, such as first-order logic, or fra…
On Compiling Structured CNFs to OBDDs
Simone Bova, Friedrich Slivovsky
We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we identify a natural sufficient condition, which we call t…