ENTCS
2007
13 years 5 months ago
2007
Bounded Model Checking (BMC) is a successful refutation method to detect errors in not only circuits and other binary systems but also in systems with more complex domains like ti...
ENTCS
2007
13 years 5 months ago
2007
Symbolic model checking is PSPACE complete. Since QBF is the standard PSPACE complete problem, it is most natural to encode symbolic model checking problems as QBF formulas and th...
ENTCS
2007
13 years 5 months ago
2007
This paper establishes undecidability of satisfiability for multi-modal logic equipped with the hybrid binder ↓ , with respect to frame classes over which the same language wit...
ENTCS
2007
13 years 5 months ago
2007
ENTCS
2007
13 years 5 months ago
2007
ed Metatheory (Extended Abstract) Andrew W. Appel Princeton University and INRIA Rocquencourt Xavier Leroy INRIA Rocquencourt We propose a benchmark to compare theorem-proving sys...
ENTCS
2007
13 years 5 months ago
2007
d Abstract) Brian Aydemir Aaron Bohannon Stephanie Weirich Department of Computer and Information Science University of Pennsylvania Philadelphia, PA, USA We explore an axiomatize...
ENTCS
2007
13 years 5 months ago
2007
Logical connectives familiar from the study of hybrid logic can be added to the logical framework LF, a constructive type theory of dependent functions. This extension turns out t...
ENTCS
2007
13 years 5 months ago
2007
Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this pape...
ENTCS
2007
13 years 5 months ago
2007
This paper proposes an extension to theorem proving interfaces for use with proofdirected debugging and other disproof-based applications. The extension is based around tracking a...
ENTCS
2007
13 years 5 months ago
2007
We describe techniques for diagnosing errors in formal equivalence checking of RTL and transistor level models of high performance microprocessors at Freescale Semiconductor Inc. ...