Bounded model checking of recursive programs with pointers in K

DOI10.1007/978-3-642-37635-1_4zbMATH Open1394.68220OpenAlexW2139533895MaRDI QIDQ2848871FDOQ2848871

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

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

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

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)

Cited In (3)

• Computer Science Logic
• Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
• Title not available (Why is that?)

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)