January 2022. Success in Software Testing (Test-Comp 2022) and Verification (SV-COMP 2022) competitions!
FuSeBMC, our white-box fuzzer for finding security vulnerabilities in programs, won 1st place in the Cover-Error category, the Cover-Branches category, and the Overall category at Test-Comp 2022
ESBMC, our SMT-based model checker for C/C++ programs acheived seventh-place among 40 state-of-the-art software verifiers at SV-COMP 2022 including 2nd place in the ReachSafety-Array, ReachSafety-ECA, and ReachSafety-XCSP subcategories.
December 2021. Simon Park and Rekha Pai have joined the team at the University of Oxford. Simon has a background in programming languages, formal verification, and model checking. Rekha’s background is in the verification of embedded systems.
November 2021. A paper reporting on further work on FlexOS has been accepted to ASPLOS 2022. A preprint and the code repository for the tool are already available.
October 2021. The FMCAD paper on End-to-End Formal Verification of a Capability Hardware Enhanced RISC-V Processor was awarded the runner-up best paper prize.
Vampire won 1st place in 3 divisions and 3rd place in 2 divisions in CASC-28, and 1st place in 3 divisions in SMT-COMP 2021.
iProver won 2nd place in one division and 3rd place in 2 divisions in CASC-28, and 1st place in one division in SMT-COMP 2021.
July 2021. Kaled Alshmrany gave an interview to SBC Channel on his work on FuSeBMC.
July 2021. A paper titled “End-to-end formal verification of a RISC-V processor extended with capability pointers” is accepted to FMCAD 2021. This case study presents the formal verification of CHERI-Flute, a modified version of Flute that implements CHERI-RISC-V, against the Sail CHERI-RISC-V specification.
May 2021. Our technical report titled “Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities” has been uploaded to TechRxiv. This report outlines our vision for a hybrid approach to protected against memory safety vulnerabilities, providing initial data and an outline of the challenges and opportunities.
April 2021. The FlexOS paper titled “FlexOS: Making OS Isolation Flexible” is accepted at HotOS 2021. This describes a novel, modular OS design whose compatmentalization and protection profile can seamlessly be tailored towards a specific application or use-case at build-time.
January 2021. Success in Software Testing (Test-Comp 2021) and Verification (SV-COMP 2021) competitions!
FuSeBMC, our white-box fuzzer for finding security vulnerabilities in programs, won 1st place in the Cover-Error category and 2nd place in the Overall category at Test-Comp 2021.
JBMC, our verification tool for Java Bytecode, won 3rd place in the Java overall category at SV-COMP 2021.
ESBMC, our SMT-based model checker for C/C++ programs, won 6th place among 25 state-of-the-art software verifiers at SV-COMP 2021. It won 1st place in one sub-category, 2nd place in four sub-categories, 4th place in the ReachSafety category, 5th place in the SoftwareSystems category.
December 2020. Fedor Shmarov joined the SCorCH team at the University of Manchester. Fedor has a background in model checking and
formal verification of stochastic hybrid systems.
November 2020. Ahmed Bhayat joined the SCorCH team at the University of Manchester. Ahmed is an expert in first-order reasoning and a contributor to the Vampire theorem proving system.