Logics, Decision Procedures, and Solvers
Satisfiability Checking for Mission-Time LTL
High-Level Abstractions for Simplifying Extended String Constraints in SMT
Alternating Automata Modulo First Order Theories
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Incremental Determinization for Quantifier Elimination and Functional Synthesis
Numerical Programs
Loop Summarization with Rational Vector Addition Systems
Invertibility Conditions for Floating-Point Formulas
Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Icing: Supporting Fast-math Style Optimizations in a Verified Compiler
Sound Approximation of Programs with Elementary Functions
Verification
Formal verification of quantum algorithms using quantum Hoare logic
SecCSL: Security Concurrent Separation Logic
Reachability Analysis for AWS-based Networks
Distributed Systems and Networks
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
Gradual Consistency Checking
Checking Robustness Against Snapshot Isolation
Efficient verification of network fault tolerance via counterexampleguided refinement
On the Complexity of Checking Consistency for Replicated Data Types
Communication-closed asynchronous protocols
Verification and Invariants
Interpolating Strong Induction
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
Inferring Inductive Invariants from Phase Structures
Termination of Triangular Integer Loops is Decidable
AliveInLean: A Verified LLVM Peephole Optimization Verifier
Concurrency
Automated Parameterized Verification of CRDTs
What's wrong with on-the-y partial order reduction
Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
Violat: Gen erating Tests of Observational Refinement for Concurrent Objects.