
ETPS
 Referenced in 160 articles
[sw06302]
 student using ETPS issues commands to apply rules of inference in specified ways ... lines of the proof and checking that the rules can be used in this...

PolyTOIL
 Referenced in 23 articles
[sw14205]
 self, and carefully defining the typechecking rules, we have obtained a language which ... used both in stating typechecking rules and expressing the bounds on type parameters ... careful formal definition of typechecking rules and semantics. A proof of type safety...

DEX
 Referenced in 12 articles
[sw27282]
 functions that are defined by decision rules; consistency checking of decision rules; acquisition, evaluation...

AGG
 Referenced in 50 articles
[sw04449]
 stepwise transformation of graphs as well as rule applications as long as possible. AGG supports ... validations which comprise graph parsing, consistency checking of graphs and conﬂict detection in concurrent transformations ... critical pair analysis of graph rules. Applications of AGG include graph and rulebased modeling...

JFlow
 Referenced in 26 articles
[sw20595]
 label model, label polymorphism, runtime label checking, and automatic label inference. JFlow also supports ... language and presents formal rules that are used to check JFlow programs for correctness. Because...

PIPER
 Referenced in 28 articles
[sw11478]
 fundamental issues in making model checking viable for software. This paper proposes new techniques ... assumeguarantee proof rule for carrying out compositional model checking on the types. Open simulation...

VAMPIRE
 Referenced in 258 articles
[sw02918]
 superposition for handling equality. The splitting rule and negative equality splitting are simulated ... used to accelerate some costly operations, e.g., checks of ordering constraints. Although the kernel...

CompCert
 Referenced in 49 articles
[sw09737]
 verified compilers come with a mathematical, machinechecked proof that the generated executable code behaves ... semantics of the source program. By ruling out the possibility of compilerintroduced bugs, verified...

VeriFlow
 Referenced in 6 articles
[sw25229]
 devices that checks for networkwide invariant violations dynamically as each forwarding rule is inserted ... VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion...

LPbook
 Referenced in 51 articles
[sw31782]
 online JAVA applets that illustrate various pivot rules and variants of the simplex method, both ... book’s webpage: http://www.princeton.edu/rvdb/LPbook/. Also, check the book’s webpage for new online...

ChC 3
 Referenced in 11 articles
[sw09781]
 modulo the given axioms A, and their rules should be (ground) coherent with E modulo ... formal verification tasks, including search, LTL model checking, and the development of abstractions, crucially depends ... interest are typed, have equations E and rules R that are both conditional, have axioms ... essential to extend the known coherence checking methods from the untyped, unconditional...

CAC
 Referenced in 1 article
[sw23324]
 tended with specific checking rules. In checking mode it detects accessibility issues...

Bedwyr
 Referenced in 22 articles
[sw09460]
 generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings ... sequent calculus by incorporating inference rules for definitions that allow fixed points to be explored ... sequent calculus can capture simple model checking problems as well as may and must behavior...

JITty
 Referenced in 5 articles
[sw10121]
 normalizing arguments and applying rewrite rules. Strategy annotations are checked for correctness...

Idris
 Referenced in 36 articles
[sw20011]
 code using the types; where clauses, with rule, simple case expressions, pattern matching ... significant syntax; Extensible syntax; Cumulative universes; Totality checking; Hugs style interactive environment...

MetTeL
 Referenced in 16 articles
[sw11990]
 flexibly specify the set of tableau rules to be used in derivations. Termination ... generalisation of a standard loop checking mechanism or unrestricted blocking...

AVal
 Referenced in 2 articles
[sw30249]
 Java5 framework for the definition and checking of rules for @OP in Java. We define...

ASPTools
 Referenced in 3 articles
[sw33089]
 program; lpshift: shift disjunctive rules into normal rules; modlist: split logic program into modules; modrun ... random planar graphs; redr: check the redundancy of individual rules in a ground logic program...

TVOC
 Referenced in 20 articles
[sw02521]
 that uses the translation validation approach to check the validity of compiler optimizations ... phase verifies loop transformations using the proof rule permute; the second phase verifies structurepreserving...

INT
 Referenced in 3 articles
[sw23776]
 manipulation package, PRESS, to check the conditions of rewrite rules and the solutions to equations...