CADE
2012
Springer
12 years 2 months ago
2012
Springer
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...
CADE
2012
Springer
12 years 2 months ago
2012
Springer
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...
CADE
2012
Springer
12 years 2 months ago
2012
Springer
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...
CADE
2012
Springer
12 years 2 months ago
2012
Springer
Abstract. This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domai...
CADE
2011
Springer
12 years 11 months ago
2011
Springer
Deduction modulo is a generic framework to describe proofs in a theory better than using raw axioms. This is done by presenting the theory through rules rewriting terms and proposi...
CADE
2011
Springer
12 years 11 months ago
2011
Springer
Abstract. We describe a new algorithm for solving linear integer programming problems. The algorithm performs a DPLL style search for a feasible assignment, while using a novel cut...
CADE
2011
Springer
12 years 11 months ago
2011
Springer
We describe asasp, a symbolic reachability procedure for the analysis of administrative access control policies. The tool represents access policies and their administrative action...
CADE
2011
Springer
12 years 11 months ago
2011
Springer
Abstract. Security protocols aim at securing communications over public networks. Their design is notoriously difficult and error-prone. Formal methods have shown their usefulness ...
CADE
2011
Springer
12 years 11 months ago
2011
Springer
This paper describes two algorithms for the compression of propositional resolution proofs. The first algorithm, RecyclePivotsWithIntersection, performs partial regularization, re...
CADE
2011
Springer
12 years 11 months ago
2011
Springer
Abstract. Sledgehammer is a component of Isabelle/HOL that employs firstorder automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically s...