Bounded model checking of recursive programs with pointers in K

DOI10.1007/978-3-642-37635-1_4MaRDI QIDQ2848871zbMATHOpenAlexFDO

Authors Irina Măriuca Asăvoae, Marcello M. Bonsangue, Dorel Lucanu, Jurriaan Rot, Frank S. de Boer

Publication date 13 September 2013

Published in Recent Trends in Algebraic Development Techniques (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37635-1_4

zbMATH Keywords

model checkingpushdown systems\(\mathbb{K}\) framework

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

• Computer Science Logic
• Efficient CTL model-checking for pushdown systems
• Efficient CTL model-checking for pushdown systems
• scientific article; zbMATH DE number 1796143
• Model checking probabilistic systems against pushdown specifications

Cited in

(3)

• Computer Science Logic
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection

Describes a project that uses

Uses Software

• K tool

This page was built for publication: Bounded model checking of recursive programs with pointers in K

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