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

automataconcurrencyproof systemsunbounded parallelismverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) 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

(23)

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

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)