FROCOS
2007
Springer
14 years 6 months ago
2007
Springer
In the last two decades we have witnessed an impressive advance in the efficiency of propositional satisfiability techniques (SAT), which has brought large and previously-intractab...
FROCOS
2007
Springer
14 years 6 months ago
2007
Springer
Abstract. Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools whic...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
Abstract. We present an overview of results on hierarchical and modular reasoning in complex theories. We show that for a special type of extensions of a base theory, which we call...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
Web services send and receive messages in XML syntax with some parts hashed, encrypted or signed, according to the WS-Security standard. In this paper we introduce a model to forma...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
We introduce a propositional encoding of the recursive path order with status (RPO). RPO is a combination of a multiset path order and a lexicographic path order which considers pe...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
Often when formalising dynamic systems, constraints such as exactly “n” of a set of values hold. In this paper, we consider reasoning about propositional linear time temporal ...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
Abstract. We investigate the extension of modal logics by bisimulation quantifiers and present a class of modal logics which is decidable when augmented with bisimulation quanti...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
We offer a transition system representing a high-level but detailed architecture for SMT solvers that combine a propositional SAT engine with solvers for multiple disjoint theorie...
FROCOS
2007
Springer
14 years 8 months ago
2007
Springer
Abstract. In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic funct...