93 citations · 250 across the 13 of their papers we have counts for
13 papers
Conflict-Driven XOR-Clause Learning (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Modern conflict-driven clause learning (CDCL) SAT solvers are very good in solving conjunctive normal form (CNF) formulas. However, some application problems involve lots of parity…
Classifying and Propagating Parity Constraints (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Parity constraints, common in application domains such as circuit verification, bounded model checking, and logical cryptanalysis, are not necessarily most efficiently solved if tr…
Simulating Parity Reasoning (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Propositional satisfiability (SAT) solvers, which typically operate using conjunctive normal form (CNF), have been successfully applied in many domains. However, in some applicatio…
Bounded Model Checking of an MITL Fragment for Timed Automata
Roland Kindermann, Tommi Junttila, Ilkka Niemelä
Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SA…
Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)
Tero Laitinen, Tommi Junttila, Ilkka Niemelä
Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instanc…
SMT-based Induction Methods for Timed Systems
Roland Kindermann, Tommi Junttila, Ilkka Niemelä
Modeling time related aspects is important in many applications of verification methods. For precise results, it is necessary to interpret time as a dense domain, e.g. using timed…