• 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 type-checking rules, we have obtained a language which ... used both in stating type-checking rules and expressing the bounds on type parameters ... careful formal definition of type-checking 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 conflict detection in concurrent transformations ... critical pair analysis of graph rules. Applications of AGG include graph and rule-based modeling...
  • JFlow

  • Referenced in 26 articles [sw20595]
  • label model, label polymorphism, run-time 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 ... assume-guarantee 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, machine-checked proof that the generated executable code behaves ... semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified...
  • VeriFlow

  • Referenced in 6 articles [sw25229]
  • devices that checks for network-wide 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 is-sues...
  • 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 structure-preserving...
  • INT

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