Sciweavers

Share
CADE
2012
Springer
7 years 9 months ago
Rewriting Induction + Linear Arithmetic = Decision Procedure
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...
Stephan Falke, Deepak Kapur
CADE
2012
Springer
7 years 9 months ago
SPARQL Query Containment under RDFS Entailment Regime
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...
Melisachew Wudage Chekol, Jérôme Euze...
CADE
2012
Springer
7 years 9 months ago
Taming Past LTL and Flat Counter Systems
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...
Stéphane Demri, Amit Kumar Dhar, Arnaud San...
CADE
2012
Springer
7 years 9 months ago
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
Abstract. This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domai...
François Bobot, Sylvain Conchon, Evelyne Co...
CADE
2011
Springer
8 years 6 months ago
Experimenting with Deduction Modulo
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...
Guillaume Burel
CADE
2011
Springer
8 years 6 months ago
Cutting to the Chase Solving Linear Integer Arithmetic
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...
Dejan Jovanovic, Leonardo Mendonça de Moura
CADE
2011
Springer
8 years 6 months ago
ASASP: Automated Symbolic Analysis of Security Policies
We describe asasp, a symbolic reachability procedure for the analysis of administrative access control policies. The tool represents access policies and their administrative action...
Francesco Alberti, Alessandro Armando, Silvio Rani...
CADE
2011
Springer
8 years 6 months ago
Deciding Security for Protocols with Recursive Tests
Abstract. Security protocols aim at securing communications over public networks. Their design is notoriously difficult and error-prone. Formal methods have shown their usefulness ...
Mathilde Arnaud, Véronique Cortier, St&eacu...
CADE
2011
Springer
8 years 6 months ago
Compression of Propositional Resolution Proofs via Partial Regularization
This paper describes two algorithms for the compression of propositional resolution proofs. The first algorithm, RecyclePivotsWithIntersection, performs partial regularization, re...
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel ...
CADE
2011
Springer
8 years 6 months ago
Extending Sledgehammer with SMT Solvers
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...
Jasmin Christian Blanchette, Sascha Böhme, La...
books