Slicing techniques for verification re-use

DOI10.1016/J.TCS.2005.06.020MaRDI QIDQ2571210zbMATH OpenOpenAlexFDO

Authors Heike Wehrheim

Publication date 1 November 2005

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

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

zbMATH Keywords

verificationtemporal logicslicingObject-Z

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Optimizing slicing of formal specifications by deductive verification
• Slicing behavior tree models for verification
• Formal Verification of Simulation Traces Using Computation Slicing
• Reuse of proofs in software verification
• Algebraic Methodology and Software Technology
• A novel formal approach to program slicing
• A vocabulary of program slicing-based techniques

Cites work

• scientific article; zbMATH DE number 2089401 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 2013587 (Why is no real title available?)
• scientific article; zbMATH DE number 2013588 (Why is no real title available?)
• scientific article; zbMATH DE number 2143088 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 1569128 (Why is no real title available?)
• scientific article; zbMATH DE number 1863159 (Why is no real title available?)
• scientific article; zbMATH DE number 1409638 (Why is no real title available?)
• A calculus of durations
• Formal Methods for Components and Objects
• Inheritance of temporal logic properties.
• Inheritance of workflows: An approach to tackling problems related to change
• Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation
• Slicing software for model construction
• Specification and verification of object-oriented programs using supertype abstraction
• Stutter-invariant temporal properties are expressible without the next-time operator
• ZB 2005: Formal Specification and Development in Z and B

Cited in

(5)

• ZB 2005: Formal Specification and Development in Z and B
• scientific article; zbMATH DE number 1832217 (Why is no real title available?)
• A proof system for adaptable class hierarchies
• Formal Methods for Components and Objects
• Verification of software product lines with delta-oriented slicing

Describes a project that uses

Uses Software

• Bandera

This page was built for publication: Slicing techniques for verification re-use

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