Duality and Primal-Dual Algorithms in Verification

CStar: Unifying Programming and Verification in C

Learning Domain-specific Languages and Synthesizing Axiomatizations

Thread-Modular Abstract Interpretation - The Local Perspective

Anvil: A General-Purpose Timing-Safe Hardware Description Language

Towards next-generation automated web development

A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games

Veil: A Framework for Automated and Interactive Verification of Transition Systems

Addressing the Saturation Effect in Compiler Testing

ICSE 2023 Dry Runs

Synthesising Recursive Functions for First-Order Model Counting

Parallel processing at a very large scale, with OCaml.

Automatically Testing Datalog Engines to find Optimization Bugs

Rust Verification by Functional Translation

Solving the Identifying Code Set Problem with Grouped Independent Support

Program Repair and Automated Programming

Sublanguages in Rhombus

Towards Data-Driven Mobile App Visual Testing

Fusing AI and Formal Methods for Automated Synthesis

Source Academy - A Community-Developed Environment for Teaching Programming

Proof Maintenance for Certified Libraries

How CPython 3.11 is Speeding Up

Effective Representation and Dissemination of Programming Knowledge

Verified Causal Broadcast with Liquid Haskell

Infrared: A Meta Bug Detector

Data-Driven Invariant Learning for Probabilistic Programs

The Power of Definitions for Model Counting and Sampling

Democratizing SAT Solving

Bugs in Quantum Computing Platforms and How to Detect them Automatically

Practical Formal Verification of Concurrent Code in the 21st Century

Exploiting partial orders and symmetries in efficient analysis of message-passing concurrency

Concurrency Unit Testing with Coyote

The Racket Way

CHRusty - Translating C to Safer Rust

Using Formal Methods to Analyze Modern Payment Protocols

A Short Introduction to Termination Analysis of Probabilistic Programs

Verification of Concurrent Programs under Release-Acquire Concurrency

Fast, optimal, and guaranteed safe synthesis for autonomous systems

The Missing Piece of Test Automation Puzzle: Explainable Deep Oracles

A Lazy Desugaring System for Evaluating Programs with Sugars

A New Approach to Recursive Function Synthesis

Taming Flaky Tests in a Non-Deterministic World

Linear-time Temporal Logic guided Greybox Fuzzing

Next Gen Automated Reasoning: Beyond “SAT Revolution” to “Beyond SAT” Revolution

Proof Repair

Proving Robustness to Data Bias

Taming Unbounded Distributed Systems with Modular, Bounded Verification

Rewrite Rule Inference Using Equality Saturation

Dual Channel Constraints and Natural Type Inference

Improving the Expressiveness of Programming Languages

Concolic Program Repair

Data-Driven Synthesis of a Provably Sound Side-Channel Analysis

BBPoly: Scalable and Modular Robustness Analysis of Deep Neural Networks

SynGuar: Guaranteeing Generalization in Programming by Example

Candid, an interface description language for blockchains

Deductive Verification for Ordinary Differential Equations

Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications

On the Design, Implementation, and Use of Laziness in R

Verified Graph Algorithms

ROBoSuSLik: Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

Programmer Tools with Program Synthesis

Retrofitting Effect Handlers to OCaml

Manthan: A Data-Driven Approach for Boolean Function Synthesis

TaintBench: Automatic Real-World Malware Benchmarking of Android Taint Analyses

Time-travel Testing of Android Apps

Towards Dynamic Oracle-guided Synthesis of Abstractions for Deep Neural Networks

CoSplit: Practical Smart Contract Sharding with Static Program Analysis

SICP JS: Ketchup on Caviar?

Automating proof by induction in Isabelle/HOL using domain-specific languages

Compiling Distributed System Models into Implementations

Towards Verifying AI Systems: Testing of Samplers

Tvide: Automated Temporal Verification of Integrated Dependent Effects

Source Academy, what's in it for you

On Incorrectness Logic

Optimal MC/DC Test Case Generation

Rinser: Concise Explanations in Static Analysis Driven Code Reviews

A Functional Proof Pearl: Inverting the Ackermann Hierarchy