Cut branches before looking for bugs: certifiably sound verification on relaxed slices

DOI10.1007/s00165-017-0439-xzbMath1380.68127OpenAlexW2762269809MaRDI QIDQ682366

Pascale Le Gall, Nikolai Kosmatov, Jean-Christophe Léchenet

Publication date: 2 February 2018

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0439-x

zbMATH Keywords

verificationprogram slicingCoq formalizationnon-terminating loopsrun-time errorstrajectory-based semantics

Mathematics Subject Classification ID

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

Related Items (2)

Fast computation of strong control dependencies ⋮ Runtime abstract interpretation for numerical accuracy and robustness

Uses Software

• Coq
• Frama-C
• SANTE
• DyTa

Cites Work

• A unifying theory of control dependence and its application to arbitrary program structures
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Transfinite semantics in the form of greatest fixpoint
• A trajectory-based strict semantics for program slicing
• Slicing for modern program structures: a theory for eliminating irrelevant loops
• Non-standard semantics for program slicing
• Slicing programs in the presence of errors
• Assertion-based slicing and slice graphs
• Theoretical foundations of dynamic program slicing
• Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices
• A vocabulary of program slicing-based techniques
• Program Slicing
• Programming Languages and Systems

This page was built for publication: Cut branches before looking for bugs: certifiably sound verification on relaxed slices