The field of formal methods and programming languages is moving towards increased integration of formal verification and programming language design. Recent developments have focused on creating more efficient and expressive formal methods, such as new type systems and verification frameworks, to improve the reliability and correctness of software systems. Notably, researchers are exploring ways to combine formal methods with machine learning and programming languages to create more robust and maintainable systems. Noteworthy papers in this area include ChopChop, which presents a programmable framework for semantically constraining the output of language models, and REFINESTAT, which introduces a language model-driven framework for probabilistic program synthesis. Additionally, researchers are making progress in applying formal methods to real-world problems, such as verifying the correctness of PLC software upgrades and analyzing the termination of linear-constraint programs.
Advances in Formal Methods and Programming Languages
Sources
ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models
A Hoare Logic for Symmetry Properties
Decision Procedure for A Theory of String Sequences
TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory
REFINESTAT: Efficient Exploration for Probabilistic Program Synthesis
Formal Verification of Isothermal Chemical Reactors
Type-Based Incorrectness Reasoning
Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny
Continuous Petri Nets for Fast Yield Computation: Polynomial-Time and MILP Approaches
From Traces to Program Incorrectness: A Type-Theoretic Approach
Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
Forall-Exists Relational Verification by Filtering to Forall-Forall
Non-Termination Proving: 100 Million LoC and Beyond
Fixed Parameter Tractable Linearizability Monitoring for Stack, Queue and Anagram Agnostic Data Types
Verifying Correctness of PLC Software during System Evolution using Model Containment Approach
Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning
A Generic and Efficient Python Runtime Verification System and its Large-scale Evaluation
Pacing Types: Safe Monitoring of Asynchronous Streams
Termination Analysis of Linear-Constraint Programs
Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs