2.8k citations
- Max Planck SocietyDE261 papers
- Saarland UniversityDE124 papers
- Technische Universität BerlinDE55 papers
- Centre National de la Recherche ScientifiqueFR41 papers
- Korea UniversityKR41 papers
- Stanford UniversityUS25 papers
- Institut national de recherche en sciences et technologies du numériqueFR24 papers
- ETH ZurichCH21 papers
- Helmholtz Center for Information SecurityDE20 papers
- Technical University of MunichDE20 papers
- Université de LorraineFR17 papers
- University of LuxembourgLU16 papers
4 papers · 2 filters
Context unification is in PSPACE
Artur Jeż
Contexts are terms with one `hole', i.e. a place in which we can substitute an argument. In context unification we are given an equation over terms with variables representing cont…
Triggered Clause Pushing for IC3
Martin Suda
We propose an improvement of the famous IC3 algorithm for model checking safety properties of finite state systems. We collect models computed by the SAT-solver during the clause p…
Variable and clause elimination for LTL satisfiability checking
Martin Suda
We study preprocessing techniques for clause normal forms of LTL formulas. Applying the mechanism of labelled clauses enables us to reinterpret LTL satisfiability as a set of purel…
A Framework for the Verification of Certifying Computations
Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn +1
Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually invol…