A Lazy Unbounded Model Checker for Event-B

article

A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software

A generic annotation inference algorithm for the safety certification of automatically generated code

An Empirical Evaluation of Automated Theorem Provers in Software Certification

Annotation Inference for Safety Certification of Automatically Generated Code (Extended Abstract)

Applying symbolic bounded model checking to the 2012 RERS greybox challenge

AutoBayes: a system for generating data analysis programs from statistical models

Automatic Certification of Kalman Filters for Reliable Code Generation

Automating component integration for web-based data analysis

Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization

article

CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory

scientific article published on 06 January 2023

CSeq: A Sequentialization Tool for C

CSeq: A concurrency pre-processor for sequential C verification tools

article published in 2013

CVExplorer: identifying candidate developers by mining and exploring their open source contributions

article

Certifiable Program Generation

Certification support for automatically generated programs

Comparison of Context-Free Grammars Based on Parsing Generated Test Data

ConceptCloud: a tagcloud browser for software archives

scholarly article published 2014

Concurrent Program Verification with Lazy Sequentialization and Interval Analysis

Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information

Context-Bounded Model Checking of LTL Properties for ANSI-C Software

Context-Bounded Model Checking with ESBMC 1.17

Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking

DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs

Deriving Safety Cases for Hierarchical Structure in Model-Based Development

article

Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code

Deriving safety cases from automatically constructed proofs

ESBMC 1.22

Empirically Successful Automated Reasoning: Applications Issue

Empirically Successful Automated Reasoning: Systems Issue

Explaining Verification Conditions

Exploratory search of academic publication and citation data using interactive tag cloud visualizations

scholarly article by Marcel Dunaiski et al published 9 January 2017 in Scientometrics

Extending Source Code Generators for Evidence-Based Software Certification

article

Fast Model-Based Fault Localisation with Test Suites

article

Fast test suite-driven model-based fault localisation with application to pinpointing defects in student programs

Fine-Grained Role- and Attribute-Based Access Control for Web Applications

Generating customized verifiers for automatically generated code

Grammar-based testing for little languages: an experience report with student compilers

scientific article published on 25 November 2020

Guest editors’ introduction

Handling Unbounded Loops with ESBMC 1.20

article by Jeremy Morse et al published 2013 in Lecture Notes in Computer Science

Higher-order transformations with nested concrete syntax

Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking

Interactive tag cloud visualization of software version control repositories

scholarly article published September 2015

Interpreting Abstract Interpretations in Membership Equational Logic

JEqualityGen

JEqualityGen

Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs

Lazy sequentialization for TSO and PSO via shared memory abstractions

article published in 2016

Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation

Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs

article

Lazy-CSeq: A Lazy Sequentialization Tool for C

MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings

MU-CSeq 0.4: Individual Memory Location Unwindings

MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings

Model checking LTL properties over ANSI-C programs with bounded traces

Monitoring aspects for the customization of automatically generated code for big-step models

Parallel bug-finding in concurrent programs via reduced interleaving instances

scholarly article published October 2017

Program Repair as Sound Optimization of Broken Programs

scholarly article published July 2009

Rapid Exploration of the Design Space During Automatic Generation of Kalman Filter Code

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

article

SMT-Based Bounded Model Checking of C++ Programs

Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints

scholarly article published 2009

Specification-Based Browsing of Software Component Libraries

Specification-based browsing of software component libraries

scholarly article

Synthesizing MPI Implementations from Functional Data-Parallel Programs

Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches

Using Fast Model-Based Fault Localisation to Aid Students in Self-Guided Program Repair and to Improve Assessment

article

Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models

VLex

Verifying Concurrent Programs by Memory Unwinding

Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker

Verifying multi-threaded software using smt-based context-bounded model checking

article

Vision: bias in systematic grammar-based test suite construction algorithms

scientific article published on 22 November 2021

Visualizing and exploring software version control repositories using interactive tag clouds over formal concept lattices

scholarly article by Gillian J. Greene et al published July 2017 in Information and Software Technology