CADE
2011
Springer
12 years 4 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 4 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 4 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 4 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 4 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 4 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...
CADE
2011
Springer
12 years 4 months ago
2011
Springer
Abstract. Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We here recast a technique to enhance t...
CADE
2011
Springer
12 years 4 months ago
2011
Springer
Android is a programming language based on Java and an operating system for embedded or mobile devices whose upper layers are written in that language. It features an extended even...