scientific article; zbMATH DE number 1954380
From MaRDI portal
zbMath1027.68616MaRDI QIDQ4415251
Publication date: 28 July 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2556/25560145.htm
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
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)
Related Items
Verification of Gap-Order Constraint Abstractions of Counter Systems, Decision procedures for flat array properties, Symbol elimination and applications to parametric entailment problems, Algebraic program analysis, Forward analysis and model checking for trace bounded WSTS, Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic, Equivalence between model-checking flat counter systems and Presburger arithmetic, On the freeze quantifier in Constraint LTL: Decidability and complexity, An automata-theoretic approach to constraint LTL, A New Acceleration-Based Combination Framework for Array Properties, Unnamed Item, Applying abstract acceleration to (co-)reachability analysis of reactive programs, Verification of gap-order constraint abstractions of counter systems, Bounded underapproximations, Expressive Power of Broadcast Consensus Protocols, Running time analysis of broadcast consensus protocols, Forward Analysis and Model Checking for Trace Bounded WSTS, Verification of population protocols, Verification of qualitative \(\mathbb Z\) constraints, Verification and falsification of programs with loops using predicate abstraction, Automatic Verification of Counter Systems With Ranking Function, Reachability in Timed Counter Systems, Unnamed Item, LTL over integer periodicity constraints, Proving Safety with Trace Automata and Bounded Model Checking, Iterating Octagons, Accelerating Interpolation-Based Model-Checking, Acceleration in Convex Data-Flow Analysis, Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs, Under-approximating loops in C programs for fast counterexample detection, Automata-Based Termination Proofs, Model-Checking Counting Temporal Logics on Flat Structures, Verification of programs with half-duplex communication, A class of polynomially solvable range constraints for interval analysis without widenings, CTL* model checking for data-aware dynamic systems with arithmetic, Taming past LTL and flat counter systems, Flat Petri nets (invited talk)
