| Active Learning of Abstract System Models from Traces using Model Checking | 0 | 0.34 | 2022 |
| Deepsynth: Automata Synthesis For Automatic Task Segmentation In Deep Reinforcement Learning | 0 | 0.34 | 2021 |
| Exposing previously undetectable faults in deep neural networks | 0 | 0.34 | 2021 |
| End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers | 0 | 0.34 | 2021 |
| Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training. | 2 | 0.36 | 2019 |
| Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters | 3 | 0.38 | 2019 |
| Effective Verification for Low-Level Software with Competing Interrupts. | 1 | 0.48 | 2018 |
| Verification of tree-based hierarchical read-copy update in the Linux kernel | 3 | 0.36 | 2018 |
| Lifting CDCL to Template-based Abstract Domains for Program Verification. | 0 | 0.34 | 2017 |
| Unbounded Safety Verification For Hardware Using Software Analyzers | 1 | 0.42 | 2016 |
| Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. | 1 | 0.35 | 2016 |
| Generating test case chains for reactive systems. | 3 | 0.40 | 2016 |
| Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version). | 0 | 0.34 | 2016 |
| Equivalence Checking Using Trace Partitioning | 1 | 0.35 | 2015 |
| Effective verification of low-level software with nested interrupts | 8 | 0.52 | 2015 |
| Hardware Verification Using Software Analyzers | 4 | 0.47 | 2015 |
| On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover. | 0 | 0.34 | 2013 |
| Chaining Test Cases for Reactive System Testing (extended version). | 1 | 0.35 | 2013 |
| Chaining Test Cases for Reactive System Testing. | 7 | 0.46 | 2013 |
| Assume-guarantee validation for STE properties within an SVA environment | 1 | 0.37 | 2009 |
| A Symbolic Execution Framework For Algorithm-Level Modelling | 0 | 0.34 | 2009 |
| A refinement approach to design and verification of on-chip communication protocols | 6 | 0.54 | 2008 |
| Automatic Abstraction in Symbolic Trajectory Evaluation | 8 | 0.67 | 2007 |
| Tool Building Requirements for an API to First-Order Solvers | 4 | 0.52 | 2006 |
| A reflective functional language for hardware design and theorem proving | 28 | 1.31 | 2006 |
| An industrially effective environment for formal hardware verification | 46 | 1.93 | 2005 |
| Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings | 23 | 3.29 | 2005 |
| The PROSPER toolkit | 4 | 0.65 | 2003 |
| An AMBA-ARM7 Formal Verification Platform | 5 | 0.51 | 2003 |
| Abstraction by Symbolic Indexing Transformations | 8 | 0.63 | 2002 |
| PROSPER - An Investigation into Software Architecture for Embedded Proof Engines | 0 | 0.34 | 2002 |
| Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings | 25 | 1.96 | 2001 |
| Practical Formal Verification in Microprocessor Design | 25 | 1.39 | 2001 |
| Formally Analyzed Dynamic Synthesis of Hardware | 7 | 0.61 | 2001 |
| An analysis of errors in interactive proof attempts | 3 | 0.60 | 2000 |
| The PROSPER Toolkit | 43 | 2.38 | 2000 |
| A Methodology for Large-Scale Hardware Verification | 24 | 2.22 | 2000 |
| Xs are for Trajectory Evaluation, Booleans are for Theorem Proving | 3 | 0.50 | 1999 |
| Dynamic Specialisation of XC6200 FPGAs by Parial Evaluation | 22 | 1.51 | 1998 |
| Interactive theorem proving: an empirical study of user activity | 9 | 0.94 | 1998 |
| Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings | 30 | 3.51 | 1994 |
| A mechanized theory of the &pi-calculus in Hol | 25 | 1.62 | 1994 |
