• KIDS

  • Referenced in 12 articles [sw15441]
  • operations are automatic except the algorithm design tactics, which require some interaction at present. Dozens...
  • miz3

  • Referenced in 11 articles [sw18631]
  • easy access to the full set of tactics and formal libraries of HOL Light...
  • ArcAngelC

  • Referenced in 6 articles [sw06338]
  • ArcAngelC: a Refinement Tactic Language for Circus. Circus is a refinement language in which specifications ... used, and by documenting them as tactics, they can be expressed and repeatedly applied ... present ArcAngelC, a language for defining such tactics; we present the language, its semantics...
  • SEPIA

  • Referenced in 7 articles [sw21585]
  • modelled using state-based models inferred from tactic sequences. These can then be traversed automatically ... provides a useful complement to existing automated tactics...
  • OptiRisk

  • Referenced in 9 articles [sw06238]
  • Liability Management, Supply Chain Management, Strategic & Tactical Management, Scheduling of Transport Asset...
  • mural

  • Referenced in 9 articles [sw23627]
  • familiar with VDM. Chapter 5 presents the tactic language which allows the user to compose...
  • CrystallBall

  • Referenced in 8 articles [sw06509]
  • Crystal Ball, you can make the right tactical decisions to reach your objectives and gain...
  • evt

  • Referenced in 8 articles [sw09805]
  • automatic proof discovery through higher-level tactics tailored to the particular task of the verification...
  • Eisbach

  • Referenced in 8 articles [sw13077]
  • evaluate its effectiveness by implementing some tactics widely-used in the seL4 verification stack...
  • Bellerophon

  • Referenced in 4 articles [sw23943]
  • Bellerophon: tactical theorem proving for hybrid systems. Hybrid systems combine discrete and continuous dynamics, which ... focus on those insights. We present a tactics language and library for hybrid systems verification ... prover. Among the automation that emerges are tactics for decomposing hybrid systems, discovering and establishing ... with syntax and semantics for the Bellerophon tactic combinator language, culminating in an example verification...
  • CITP

  • Referenced in 7 articles [sw25269]
  • customised by the user, or the basic tactics can be applied step-by-step...
  • Coquet

  • Referenced in 6 articles [sw09919]
  • circuits, and a meaning function. We propose tactics that ease the reasoning about the behavior...
  • IsaFoR

  • Referenced in 6 articles [sw10106]
  • system. We automate this reduction via suitable tactics which we added to the IsaFoR library...
  • Tactician

  • Referenced in 6 articles [sw17591]
  • refactor the ML of a tactic proof, typically to package up a ”g/e” style proof...
  • EXPANDER

  • Referenced in 6 articles [sw22715]
  • implement specific proof plans, strategies or tactics. It is written in the functional language SML/NJ...
  • Rtac

  • Referenced in 3 articles [sw13124]
  • Rtac – a reflective tactic language for Coq. Computational reflection is a useful technique for avoiding ... write reflective procedures than the equivalent tactics. Can we build a lightweight tactic language ... present Rtac, a lightweight, work-in-progress, tactic language built on top of MirrorCore...
  • MMode

  • Referenced in 3 articles [sw24341]
  • Abstract. We present a set of tactics for version 7.4 of the Coq proof assistant ... proof language of the Mizar system. These tactics can be used with any interface ... freely mixed with the normal Coq tactics...
  • MCTS-Solver

  • Referenced in 5 articles [sw00565]
  • Solver, has been designed to play narrow tactical lines better in sudden-death games such...
  • Galculator

  • Referenced in 5 articles [sw09979]
  • When combined with the pointfree transform and tactics such as the indirect equality principle, Galois...
  • LLNet

  • Referenced in 5 articles [sw42507]
  • light Image Enhancement. In surveillance, monitoring and tactical reconnaissance, gathering the right visual information from...