We propose a new logic, called differential dynamic game logic (dDGL), that adds several game constructs on top of differential dynamic logic (dL) so that it can be used for hybr...
Combination of theories underlies the design of satisfiability modulo theories (SMT) solvers. The Nelson-Oppen framework can be used to build a decision procedure for the combinat...
Pascal Fontaine, Stephan Merz, Christoph Weidenbac...
We propose a word level, bounded model checking (BMC) algorithm based on translation into the effectively propositional fragment (EPR) of firstorder logic. This approach to BMC al...
Moshe Emmer, Zurab Khasidashvili, Konstantin Korov...
We introduce a technique to prove non-termination of term rewrite systems automatically. Our technique improves over previous approaches substantially, as it can also detect non-lo...
Abstract. This paper presents new results on the decidability of inductive validity of conjectures. For these results, a class of term rewrite systems (TRSs) with built-in linear i...
The problem of SPARQL query containment is defined as determining if the result of one query is included in the result of another for any RDF graph. Query containment is important...
Abstract. Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known c...
Abstract. This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domai...