CADE
2008
Springer
14 years 4 months ago
2008
Springer
Abstract. A proof method is described which combines compositional proofs of interleaved parallel programs with the intuitive and highly automatic strategy of symbolic execution. A...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Many safety- and security-critical systems are real-time systems and, as a result, tools and techniques for verifying real-time systems are extremely important. Simulation and test...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
We present a tool for automatic generation of packed bitfields and tagged unions for systems-level C, along with automatic, machine checked refinement proofs in Isabelle/HOL. Our a...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Abstract. Operating-system verification gains increasing research interest. The complexity of such systems is, however, challenging and many endeavors are limited in some respect: ...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Confidentiality is maybe the most popular security property to be formally or informally verified. Noninterference is a baseline security policy to formalize confidentiality of sec...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Rely-guarantee (RG) reasoning is useful for modular Hoare-style proofs of concurrent programs. However, RG requires that assertions be proved stable under the actions of the enviro...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Abstract. The LogAnswer system is an application of automated reasoning to the field of open domain question-answering, the retrieval of answers to natural language questions regar...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Bit vectors and bit operations are proposed for efficient propositional inference. Bit arithmetic has efficient software and hardware implementations, which can be put to advantage...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
Collaborative Programming is characterized by groups of people issuing instructions to computer systems. Collaborative Programming languages differ from traditional programming lan...