Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
58 | Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001 |
Unifying Theories in ProofPower-Z. |
UTP |
2006 |
DBLP DOI BibTeX RDF |
Unifying Theories of Programming, theorem prover |
58 | Vincent Zammit |
On the Implementation of an Extensible Declarative Proof Language. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
58 | Vincent Zammit |
A Comparative Study of Coq and HOL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
50 | Wing Lam, Sara Jones 0001 |
Mechanising Requirements Engineering: Reuse and the Application of Domain Analysis Technology. |
ASE |
1997 |
DBLP DOI BibTeX RDF |
requirements engineering mechanisation, domain analysis technology, industrial avionics domain, application domain analysis, task domain analysis, formal specification, reuse |
49 | Andrew D. Gordon 0001 |
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. |
HUG |
1993 |
DBLP DOI BibTeX RDF |
|
31 | Eerke A. Boiten, John Derrick, Gerhard Schellhorn |
Relational concurrent refinement part II: Internal operations and outputs. |
Formal Aspects Comput. |
2009 |
DBLP DOI BibTeX RDF |
Process algebraic semantics, Failures-divergences refinement, Internal operations, Mechanisation, KIV, Simulations, Deadlock, Z, Data refinement, Outputs |
31 | Michael Jackson 0001 |
Automated software engineering: supporting understanding. |
Autom. Softw. Eng. |
2008 |
DBLP DOI BibTeX RDF |
Mechanisation, Complexity, Automation, Fragmentation, Manipulation, Description |
30 | Hongying Wang, Bing Sun |
Mechanisation and path analysis of dominant technology in emerging energy industry - based on CA model and fsQCA method. |
Int. J. Technol. Manag. |
2023 |
DBLP DOI BibTeX RDF |
|
30 | Hing-Lun Chan, Michael Norrish |
Mechanisation of the AKS Algorithm. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
30 | Uma Zalakain, Ornela Dardha |
π with Leftovers: A Mechanisation in Agda. |
FORTE |
2021 |
DBLP DOI BibTeX RDF |
|
30 | Chengdai Huang, Jinde Cao |
Bifurcation Mechanisation of a Fractional-Order Neural Network with Unequal Delays. |
Neural Process. Lett. |
2020 |
DBLP DOI BibTeX RDF |
|
30 | Uma Zalakain, Ornela Dardha |
π with leftovers: a mechanisation in Agda. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
30 | Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber |
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. |
LFMTP |
2020 |
DBLP DOI BibTeX RDF |
|
30 | Daniela Lovarelli, Marco Fiala, Gunnar Larsson |
Fuel consumption and exhaust emissions during on-field tractor activity: A possible improving strategy for the environmental load of agricultural mechanisation. |
Comput. Electron. Agric. |
2018 |
DBLP DOI BibTeX RDF |
|
30 | Andrea Mannocci, Angelo Antonio Salatino, Francesco Osborne, Enrico Motta |
2100 AI: Reflections on the Mechanisation of Scientific Discovery. |
BlackMirror@ISWC |
2017 |
DBLP BibTeX RDF |
|
30 | Hing-Lun Chan, Michael Norrish |
Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
30 | Seyed H. Haeri |
Component-based mechanisation of programming languages in embedded settings. |
|
2015 |
RDF |
|
30 | Aditi Barthwal, Michael Norrish |
A mechanisation of some context-free language theory in HOL4. |
J. Comput. Syst. Sci. |
2014 |
DBLP DOI BibTeX RDF |
|
30 | Seyed H. Haeri, Sibylle Schupp |
Reusable Components for Lightweight Mechanisation of Programming Languages. |
SC@STAF |
2013 |
DBLP DOI BibTeX RDF |
|
30 | Matthew J. Lovert |
On the mechanisation of the logic of partial functions. |
|
2013 |
RDF |
|
30 | Manfred Kerber, Michael Kohlhase |
Reasoning without believing: on the mechanisation of presuppositions and partiality. |
J. Appl. Non Class. Logics |
2012 |
DBLP DOI BibTeX RDF |
|
30 | Aditi Barthwal, Michael Norrish |
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. |
WoLLIC |
2010 |
DBLP DOI BibTeX RDF |
|
30 | Howard Rosenbrock |
Ethics, science, and the mechanisation of the world picture. |
AI Soc. |
2004 |
DBLP DOI BibTeX RDF |
Taylorism, Work design, Causality, Purpose, Quantum theory |
30 | David John Clark |
Enclosing the field : from 'mechanisation of thought processes' to 'autonomics'. |
|
2002 |
RDF |
|
30 | René Vestergaard, James Brotherston |
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). |
MERLIN |
2001 |
DBLP DOI BibTeX RDF |
|
30 | Jeremy E. Dawson, Rajeev Goré |
A Mechanisation of Classical Modal Tense Logics Using Isabelle. |
Australian Joint Conference on Artificial Intelligence |
1998 |
DBLP DOI BibTeX RDF |
logics for knowledge and belief, display logic, sequent calculus, automated deduction, hybrid logics, tense logic |
30 | Vincent Zammit |
A Mechanisation of Computability Theory in HOL. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
30 | William L. Harrison, Myla Archer, Karl N. Levitt |
A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
30 | Andrew Stevens 0001 |
An improved method for the mechanisation of inductive proof. |
|
1989 |
RDF |
|
30 | P. Seetharamaiah, V. R. Murthy |
Tabular Mechanisation for Flexible Testing of Microprocessors. |
ITC |
1986 |
DBLP BibTeX RDF |
|
19 | Harvey Tuch |
Formal Verification of C Systems Code. |
J. Autom. Reason. |
2009 |
DBLP DOI BibTeX RDF |
C, Separation logic, Interactive theorem proving |
19 | Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001 |
A UTP semantics for Circus. |
Formal Aspects Comput. |
2009 |
DBLP DOI BibTeX RDF |
Concurrency, Theorem proving, Relational model, Refinement calculus |
19 | Aditi Barthwal, Michael Norrish |
Verified, Executable Parsing. |
ESOP |
2009 |
DBLP DOI BibTeX RDF |
|
19 | Frank Zeyda, Ana Cavalcanti 0001 |
Mechanised Translation of Control Law Diagrams into Circus. |
IFM |
2009 |
DBLP DOI BibTeX RDF |
ClawZ, verification, CSP, Z, Simulink |
19 | Leo Freitas |
Mechanising Data-Types for Kernel Design in Z. |
SBMF |
2009 |
DBLP DOI BibTeX RDF |
|
19 | Alexei Iliasov |
Refinement patterns for rapid development of dependable systems. |
EFTS |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Leo Freitas, Zheng Fu, Jim Woodcock 0001 |
POSIX file store in Z/Eves: an experiment in the verified software repository. |
ICECCS |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Michael Norrish |
Mechanising lambda-calculus using a classical first order theory of terms with permutations. |
High. Order Symb. Comput. |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Annabelle McIver, Tjark Weber |
Towards Automated Proof Support for Probabilistic Distributed Systems. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Michael Norrish |
Mechanising Hankin and Barendregt using the Gordon-Melham axioms. |
MERLIN |
2003 |
DBLP DOI BibTeX RDF |
higher order abstract syntax, interactive theorem-proving |
19 | Linas Laibinis, Joakim von Wright |
Functional Procedures in Higher-Order Logic. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
19 | Monica Nesi |
Formalising a Value-Passing Calculus in HOL. |
Formal Aspects Comput. |
1999 |
DBLP DOI BibTeX RDF |
Meta-theoretic reasoning, Formal verification, Theorem proving, Higher order logic, Process calculi |
19 | Jacques D. Fleuriot, Lawrence C. Paulson |
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
19 | Clare Dixon, Michael Fisher 0001 |
The Set of Support Strategy in Temporal Resolution. |
TIME |
1998 |
DBLP DOI BibTeX RDF |
|
19 | Jeremy E. Dawson, Rajeev Goré |
A Mechanised Proof System for Relation Algebra using Display Logic. |
JELIA |
1998 |
DBLP DOI BibTeX RDF |
|
19 | Daniel Hirschkoff |
A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
19 | Clare Dixon |
Search Strategies for Resolution in Temporal Logics. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|