- Referenced in 14 articles
- unifying theories of programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation ... firstly, a deep semantic model of UTP’s alphabetised predicates, supporting meta-logical reasoning that ... mathematical structures in Isabelle to proofs about UTP theories. Additionally, our work provides novel insights...
- Referenced in 13 articles
- unifying theories of programming (UTP). We develop a machine-checked, formal semantics based ... Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules...
- Referenced in 5 articles
- Programming Theorem Prover ( U·(TP)2, ”UTP-squared”, or UTP2 if stuck in ASCII-land ... Unifying Theories of Programming framework (UTP). Formerly known as Saoithín (pronounced ”See-heen”) Saoithín ... support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support ... that is prevalent in much of the UTP literature, from the seminal work by Hoare...
- Referenced in 4 articles
- support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support ... that is prevalent in much of the UTP literature, from the seminal work by Hoare ... features include: a formalisation of a UTP Theory; support for common proof strategies; sophisticated goal/law...
- Referenced in 2 articles
- UTPCalc -- a calculator for UTP predicates. We present the development of the UTP-Calculator ... someone who is both very familiar with UTP theory construction, and familiar enough with Haskell...
- Referenced in 1906 articles
- Coq is a formal proof management system. It...
- Referenced in 719 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 13702 articles
- MATLAB® is a high-level language and interactive...
- Referenced in 64 articles
- Nitpick is a counterexample generator for Isabelle/HOL that...
- Referenced in 524 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 14 articles
- ArcAngel: a tactic language for refinement. Morgan’s...
- Referenced in 264 articles
- Vampire 8.0, [RV02,Vor05] is an automatic theorem...
- Referenced in 8 articles
- XML-based static type checking and dynamic visualization...
- Referenced in 727 articles
- Spin is a popular open-source software tool...
- Referenced in 634 articles
- PVS is a verification system: that is, a...
- Referenced in 185 articles
- SPASS is an automated theorem prover for first...
- Referenced in 19 articles
- Maria: Modular reachability analyser for algebraic system nets...
- Referenced in 44 articles
- The Daikon system for dynamic detection of likely...
- Referenced in 820 articles
- Simulink® is an environment for multidomain simulation and...