Verification as a parameterized testing (experiments with the SCP4 supercompiler)

DOI10.1134/S0361768807010033MaRDI QIDQ2371554zbMATH OpenOpenAlexFDO

Authors A. P. Nemytykh, Alexej P. Lisitsa

Publication date 5 July 2007

Published in Programming and Computer Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1134/s0361768807010033

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION
• scientific article; zbMATH DE number 1615262
• ParaVerifier: an automatic framework for proving parameterized cache coherence protocols
• On one application of computations with oracle
• scientific article; zbMATH DE number 4024753

Cites work

• Constraint-based verification of parameterized cache coherence protocols
• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• The automation of proof by mathematical induction
• The concept of a supercompiler
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(9)

• On one application of computations with oracle
• Higher-level supercompilation as a metasystem transition
• Intermediate representation of programs with type specification based on pattern matching
• scientific article; zbMATH DE number 1615262 (Why is no real title available?)
• Supercompilation for Martin-Lof's type theory
• Certifying supercompilation for Martin-Löf's type theory
• REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION
• Automatic result verification by complete run-time checking of computations
• Ping-pong protocols as prefix grammars: modelling and verification via program transformation

Describes a project that uses

Uses Software

• Refal

This page was built for publication: Verification as a parameterized testing (experiments with the SCP4 supercompiler)

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