Proof spaces for unbounded parallelism

DOI10.1145/2676726.2677012MaRDI QIDQ2819827zbMATH OpenOpenAlexFDO

Authors Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2676726.2677012

zbMATH Keywords

verificationautomataconcurrencyproof systemsunbounded parallelism

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 786499
• scientific article; zbMATH DE number 2064226
• Infinets: the parallel syntax for non-wellfounded proof-theory
• scientific article; zbMATH DE number 937366
• Abstractions of uniform proofs
• Hyperincursive proof theory
• A proof theory for general unification
• Classical proofs as parallel programs
• A framework for space complexity in algebraic proof systems
• Unified correspondence as a proof-theoretic tool

Cited in

(22)

• Thread modularity at many levels: a pearl in compositional verification
• Verifying the correctness of distributed systems via mergeable parallelism
• What's decidable about program verification modulo axioms?
• Regression verification for multi-threaded programs
• Automating Verification of Loops by Parallelization
• Domains for Higher-Order Games
• Automated program verification
• Causality-based verification of multi-threaded programs
• Verification by Parallelization of Parametric Code
• Proving liveness of parameterized programs
• A dynamic logic for deductive verification of multi-threaded programs
• Proof-guided underapproximation-widening for multi-process systems
• Efficient coverability analysis by proof minimization
• Unbounded-thread program verification using thread-state equations
• Choose your proofs: commutativity and symmetry for smarter reasoning
• Compositional termination proofs for multi-threaded programs
• Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Constraint-based automatic verification of abstract models of multithreaded programs
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Abstract threads
• Proofs that count

Describes a project that uses

Uses Software

• CEGAR

This page was built for publication: Proof spaces for unbounded parallelism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819827)