Advances in Formal Methods and Logic for Complex Systems

The field of formal methods and logic is experiencing significant advancements, driven by the need to analyze and verify complex systems. Recent developments focus on improving the expressiveness and effectiveness of formal languages and logics, allowing for more accurate modeling and reasoning about intricate systems. Notably, research explores the integration of probabilistic and temporal aspects into traditional formal methods, enabling the analysis of systems under uncertainty and time-dependent behavior. Furthermore, innovations in separation logic and type systems facilitate the verification of complex programs and distributed systems. The field also sees advancements in query languages and data structures, enabling more efficient and scalable analysis of large datasets and temporal networks. Overall, these developments aim to provide more robust and scalable formal methods for designing, verifying, and analyzing complex systems. Noteworthy papers include: Project-connex Decompositions and Tractability of Aggregate Group-by Conjunctive Queries, which introduces a novel measure for tractability in query evaluation. Timetide: A programming model for logically synchronous distributed systems, which presents a novel programming model for deterministic distribution without physical clock synchronization. Mayura: Exploiting Similarities in Motifs for Temporal Co-Mining, which proposes a framework for unified mining of multiple temporal motifs. Bayesian Separation Logic, which introduces a probabilistic separation logic for reasoning about Bayesian probabilistic programming languages.

Sources

Project-connex Decompositions and Tractability of Aggregate Group-by Conjunctive Queries

Timetide: A programming model for logically synchronous distributed systems

Mayura: Exploiting Similarities in Motifs for Temporal Co-Mining

STL-GO: Spatio-Temporal Logic with Graph Operators for Distributed Systems with Multiple Network Topologies

Bayesian Separation Logic

An Adequate While-Language for Stochastic Hybrid Computation

A Unifying Framework for Semiring-Based Constraint Logic Programming With Negation (full version)

Triadic First-Order Logic Queries in Temporal Networks

Integrating Belief Domains into Probabilistic Logic Programs

Realisability and Complementability of Multiparty Session Types

A large-scale distributed parallel discrete event simulation engines based on Warped2 for Wargaming simulation

Fagin's Theorem for Semiring Turing Machines

Built with on top of