How to compose Presburger-accelerations: Applications to broadcast protocols

DOI10.1007/3-540-36206-1_14MaRDI QIDQ4415251zbMATH OpenFDO

Authors Jérôme Leroux, Alain Finkel

Publication date 28 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2556/25560145.htm

zbMATH Keywords

accelerationinfinite-state systemsPresburger model checkingreachability setverification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Systematic Acceleration in Regular Model Checking
• About \textsc{Fast} and \textsc{TReX} accelerations
• Acceleration for Petri nets
• Well-abstracted transition systems (extended abstract)

Cited in

(42)

• CTL* model checking for data-aware dynamic systems with arithmetic
• Flat Petri nets (invited talk)
• Running time analysis of broadcast consensus protocols
• Taming past LTL and flat counter systems
• Verification of gap-order constraint abstractions of counter systems
• LTL over integer periodicity constraints
• Verification of programs with half-duplex communication
• A class of polynomially solvable range constraints for interval analysis without widenings
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Decision procedures for flat array properties
• Verification of gap-order constraint abstractions of counter systems
• Forward analysis and model checking for trace bounded WSTS
• A new acceleration-based combination framework for array properties
• Forward analysis and model checking for trace bounded WSTS
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Iterating Octagons
• Automata-Based Termination Proofs
• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• Bounded underapproximations
• Affine extensions of integer vector addition systems with states
• scientific article; zbMATH DE number 7559502 (Why is no real title available?)
• Model-Checking Counting Temporal Logics on Flat Structures
• Automatic verification of counter systems with ranking function
• Reachability in timed counter systems
• Proving safety with trace automata and bounded model checking
• Verification of population protocols
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Technology for Verification and Analysis
• Accelerating Interpolation-Based Model-Checking
• Acceleration in Convex Data-Flow Analysis
• Expressive Power of Broadcast Consensus Protocols
• On simulating Turing machines with matrix semigroups with integrality tests
• Reasoning about reversal-bounded counter machines
• On the complexity of proving polyhedral reductions
• Under-approximating loops in C programs for fast counterexample detection
• Symbol elimination and applications to parametric entailment problems
• Algebraic program analysis
• On the freeze quantifier in Constraint LTL: Decidability and complexity
• An automata-theoretic approach to constraint LTL
• Verification of qualitative \(\mathbb Z\) constraints
• Verification and falsification of programs with loops using predicate abstraction

This page was built for publication: How to compose Presburger-accelerations: Applications to broadcast protocols

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