Reducing behavioural to structural properties of programs with procedures

DOI10.1016/J.TCS.2013.02.006MaRDI QIDQ385023zbMATH OpenOpenAlexFDO

Authors Dilian Gurov, Marieke Huisman

Publication date 29 November 2013

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2013.02.006

zbMATH Keywords

program verificationcompositional reasoningcontrol-flow behaviourcontrol-flow structuremodal \(\mu\)-calculussafety properties

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Reducing Behavioural to Structural Properties of Programs with Procedures
• Compositional verification of sequential programs with procedures
• Compositional characterization of observable program properties
• Model checking procedural programs
• Program structures: Some new characterisations

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 176726 (Why is no real title available?)
• scientific article; zbMATH DE number 1033559 (Why is no real title available?)
• scientific article; zbMATH DE number 2087443 (Why is no real title available?)
• scientific article; zbMATH DE number 2087509 (Why is no real title available?)
• -Calculus with Explicit Points and Approximations
• A fixpoint calculus for local and global program flows
• An automata theoretic decision procedure for the propositional mu- calculus
• CVPP: a tool set for compositional verification of control-flow safety properties
• Compositional verification of sequential programs with procedures
• Decidability of DPDA equivalence
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Fundamental Approaches to Software Engineering
• Graphical versus logical specifications
• Languages of Nested Trees
• MAVEN: Modular Aspect Verification
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Modular specification and verification of object-oriented programs
• On the power of abstract interpretation
• ProMoVer: modular verification of temporal safety properties
• Reducing Behavioural to Structural Properties of Programs with Procedures
• Results on the propositional \(\mu\)-calculus
• Temporal reasoning for procedural programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification on infinite structures.
• Weighted pushdown systems and their application to interprocedural dataflow analysis

Cited in

(3)

• A theory of reduced and minimal procedural dependencies
• Reducing Behavioural to Structural Properties of Programs with Procedures
• CVPP: a tool set for compositional verification of control-flow safety properties

Describes a project that uses

Uses Software

• MAVEN
• ProMoVer

This page was built for publication: Reducing behavioural to structural properties of programs with procedures

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