Paper Info
Title
The Bedwyr System for Model Checking over Syntactic Expressions
Abstract
Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference rules for definitionsthat allow fixed pointsto be explored. As a result, proof search in such a sequent calculus can capture simple model checking problems as well as may and must behavior in operational semantics. The second is that higher-order abstract syntax is directly supported using term-level 茂戮驴-binders and the 茂戮驴 quantifier. These features allow reasoning directly on expressions containing bound variables.
Year
DOI
Venue
2007
10.1007/978-3-540-73595-3_28
conference on automated deduction
Keywords
DocType
Volume
sequent calculus,operational semantics,fixed point,inference rule,model checking
Conference
abs/cs/0702116
ISSN
Citations 
PageRank 
CADE 2007: 21th Conference on Automated Deduction, Frank Pfenning, editor, LNAI 4603, pages 391-397. Springer, 2007
40
1.35
References 
Authors
9
5
Name
Order
Citations
PageRank
David Baelde115513.37
Andrew Gacek225216.87
Dale Miller32485232.26
Gopalan Nadathur41047117.85
Alwen Fernanto Tiu561043.00