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

DOI10.1134/S0361768807010033zbMath1120.68383OpenAlexW2003823454MaRDI QIDQ2371554

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)

Related Items

Supercompilation for Martin-Lof's type theory ⋮ Certifying Supercompilation for Martin-Löf’s Type Theory ⋮ REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION ⋮ Intermediate representation of programs with type specification based on pattern matching ⋮ On one application of computations with oracle ⋮ Higher-level supercompilation as a metasystem transition ⋮ Ping-pong protocols as prefix grammars: modelling and verification via program transformation

Uses Software

• Refal

Cites Work

• Constraint-based verification of parameterized cache coherence protocols
• The concept of a supercompiler
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Unnamed Item
• Unnamed Item