On the public citation graph
Software model checking: extracting verification models from source code†
0 signed · 153 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1002/bltj.2103openalex-snapshot
Systematic software testing using VeriSoft-An analysis of the 4ESS™ heart-beat monitor
inferredcites →https://doi.org/10.1002/bltj.2130openalex-snapshot
The PathStar access server: Facilitating carrier-scale packet telephony
inferredcites →https://doi.org/10.1002/bltj.2223openalex-snapshot
Automating software feature verification
inferredcites →https://doi.org/10.1007/10722468_7openalex-snapshot
Bebop: A Symbolic Model Checker for Boolean Programs
inferredcites →https://doi.org/10.1007/10722468_8openalex-snapshot
Logic Verification of ANSI-C Code with SPIN
inferredcites →https://doi.org/10.1007/s100090050043openalex-snapshot
Model checking JAVA programs using JAVA PathFinder
inferredcites →https://doi.org/10.1109/32.708566openalex-snapshot
Model checking large software specifications
inferredcites →https://doi.org/10.1145/239098.239127openalex-snapshot
Model checking large software specifications
inferredcites →https://doi.org/10.1145/298595.298598openalex-snapshot
Property specification patterns for finite-state verification
inferredcites →https://doi.org/10.1145/298595.298864openalex-snapshot
Designing executable abstractions
inferredcites →https://doi.org/10.1145/302405.302710openalex-snapshot
A practical method for verifying event-driven software
inferredcites →https://doi.org/10.5555/381473.381493openalex-snapshot
Tool-supported program abstraction for finite-state verification
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1002/bltj.2206openalex-snapshot
Software verification at Bell Labs: One line of development
inferred← citeshttps://doi.org/10.1002/cpe.1068openalex-snapshot
Towards a framework and a benchmark for testing tools for multi‐threaded programs
inferred← citeshttps://doi.org/10.1002/spe.2910openalex-snapshot
Finite‐state model extraction and visualization from Java program execution
inferred← citeshttps://doi.org/10.1002/stvr.422openalex-snapshot
Verification support for ARINC‐653‐based avionics software
inferred← citeshttps://doi.org/10.1002/stvr.439openalex-snapshot
Automated verification and testing of user‐interactive undo features in database applications
inferred← citeshttps://doi.org/10.1007/10722468_13openalex-snapshot
A Language Framework for Expressing Checkable Properties of Dynamic Software
inferred← citeshttps://doi.org/10.1007/11691617_11openalex-snapshot
Abstract Matching for Software Model Checking
inferred← citeshttps://doi.org/10.1007/3-540-36135-9_17openalex-snapshot
C Wolf - A Toolset for Extracting Models from C Programs
inferred← citeshttps://doi.org/10.1007/3-540-44585-4_15openalex-snapshot
Verifying Network Protocol Implementations by Symbolic Refinement Checking
inferred← citeshttps://doi.org/10.1007/3-540-44947-7_12openalex-snapshot
Quasar: A New Tool for Concurrent Ada Programs Analysis
inferred← citeshttps://doi.org/10.1007/3-540-45441-1_6openalex-snapshot
Timing Analysis of UML Activity Diagrams
inferred← citeshttps://doi.org/10.1007/3-540-45449-7_8openalex-snapshot
Verification of Embedded Software: Problems and Perspectives
inferred← citeshttps://doi.org/10.1007/978-3-031-31476-6_8openalex-snapshot
The Role of Abstraction in Model Checking
inferred← citeshttps://doi.org/10.1007/978-3-031-57249-4_3openalex-snapshot
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
inferred← citeshttps://doi.org/10.1007/978-3-319-23820-3_28openalex-snapshot
Rigorous Examination of Reactive Systems:
inferred← citeshttps://doi.org/10.1007/978-3-319-47169-3_59openalex-snapshot
RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification
inferred← citeshttps://doi.org/10.1007/978-3-540-24622-0_17openalex-snapshot
Static Analysis versus Software Model Checking for Bug Finding
inferred← citeshttps://doi.org/10.1007/978-3-540-30232-2_6openalex-snapshot
Localizing Program Errors for Cimple Debugging
inferred← citeshttps://doi.org/10.1007/978-3-540-30482-1_22openalex-snapshot
Software Model Checking Using Linear Constraints
inferred← citeshttps://doi.org/10.1007/978-3-540-73370-6_16openalex-snapshot
Model Extraction for ARINC 653 Based Avionics Software
inferred← citeshttps://doi.org/10.1007/978-3-540-93900-9_10openalex-snapshot
Model-Checking the Linux Virtual File System
inferred← citeshttps://doi.org/10.1007/978-3-642-28891-3_25openalex-snapshot
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
inferred← citeshttps://doi.org/10.1007/978-3-642-34026-0_45openalex-snapshot
The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems
inferred← citeshttps://doi.org/10.1007/978-3-642-39176-7_2openalex-snapshot
Proving Properties of Concurrent Programs
inferred← citeshttps://doi.org/10.1007/978-3-662-49674-9_43openalex-snapshot
Scalable Verification of Linear Controller Software
inferred← citeshttps://doi.org/10.1007/978-3-662-54577-5_9openalex-snapshot
Automatic Verification of Finite Precision Implementations of Linear Controllers
inferred← citeshttps://doi.org/10.1007/978-81-322-2247-7_40openalex-snapshot
Automatic Model Extraction from C Code—Abstracter and Architecture
inferred← citeshttps://doi.org/10.1007/978-981-99-1203-2_13openalex-snapshot
Reporting Code Coverage at Requirement Phase Using SPIN Model Checker
inferred← citeshttps://doi.org/10.1007/s001650300004openalex-snapshot
Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol
inferred← citeshttps://doi.org/10.1007/s10009-009-0106-5openalex-snapshot
Model checking C source code for embedded systems
inferred← citeshttps://doi.org/10.1007/s10009-009-0112-7openalex-snapshot
Checking the reliability of socket based communication software
inferred← citeshttps://doi.org/10.1007/s10009-010-0155-9openalex-snapshot
Model checking software: on some new waves and some evergreens
inferred← citeshttps://doi.org/10.1007/s10009-014-0337-yopenalex-snapshot
Rigorous examination of reactive systems
inferred← citeshttps://doi.org/10.1007/s10009-021-00617-zopenalex-snapshot
The RERS challenge: towards controllable and scalable benchmark synthesis
inferred← citeshttps://doi.org/10.1007/s10270-003-0042-xopenalex-snapshot
Formal verification of software source code through semi-automatic modeling
inferred← citeshttps://doi.org/10.1007/s10270-015-0466-0openalex-snapshot
Using contexts to extract models from code
inferred← citeshttps://doi.org/10.1007/s10586-017-0757-zopenalex-snapshot
Software model checking for resources race
inferred← citeshttps://doi.org/10.1007/s10586-026-06433-xopenalex-snapshot
A Configurable FPGA SIMD architecture for FSM-oriented software testing acceleration
inferred← citeshttps://doi.org/10.1007/s10703-005-1491-3openalex-snapshot
Translating Java for Multiple Model Checkers: The Bandera Back-End
inferred← citeshttps://doi.org/10.1007/s10703-006-0002-5openalex-snapshot
Feature interaction detection by pairwise analysis of LTL properties—A case study
inferred← citeshttps://doi.org/10.1007/s10817-009-9124-yopenalex-snapshot
Model Checking Dynamic Memory Allocation in Operating Systems
inferred← citeshttps://doi.org/10.1007/s10990-008-9032-6openalex-snapshot
Types and trace effects for object orientation
inferred← citeshttps://doi.org/10.1016/j.advengsoft.2012.12.004openalex-snapshot
Software simulation and verification to increase the reliability of Intelligent Environments
inferred← citeshttps://doi.org/10.1016/j.comnet.2006.08.009openalex-snapshot
A template-based approach for the generation of abstractable and reducible models of featured networks
inferred← citeshttps://doi.org/10.1016/j.entcs.2004.06.010openalex-snapshot
Model Checking Multithreaded Programs by Means of Reduced Models
inferred← citeshttps://doi.org/10.1016/j.entcs.2006.01.008openalex-snapshot
Checking Event-Based Specifications in Java Systems
inferred← citeshttps://doi.org/10.1016/j.entcs.2013.07.006openalex-snapshot
Distributed LTL Model Checking with Hash Compaction
inferred← citeshttps://doi.org/10.1016/j.infsof.2008.08.003openalex-snapshot
Model-checking for adventure videogames
inferred← citeshttps://doi.org/10.1016/j.jcss.2004.11.001openalex-snapshot
A local approach for temporal model checking of Java bytecode
inferred← citeshttps://doi.org/10.1016/j.procs.2018.08.118openalex-snapshot
Verification and online updating of decision making control logic for onboard real-time control systems
inferred← citeshttps://doi.org/10.1016/j.proeng.2015.11.498openalex-snapshot
A Comprehensive Safety Engineering Approach for Software-Intensive Systems Based on STPA
inferred← citeshttps://doi.org/10.1016/s0065-2458(05)65002-4openalex-snapshot
Software Model Checking with Spin
inferred← citeshttps://doi.org/10.1016/s0141-9331(03)00127-3openalex-snapshot
Formula-based abstractions and symbolic execution for model checking programs
inferred← citeshttps://doi.org/10.1016/s1389-1286(02)00352-3openalex-snapshot
Feature interaction: a critical review and considered forecast
inferred← citeshttps://doi.org/10.1016/s1571-0661(04)00258-0openalex-snapshot
Model Checking the Garbage Collection Mechanism of SMV
inferred← citeshttps://doi.org/10.1016/s1571-0661(04)00261-0openalex-snapshot
Trail-Directed Model Checking
inferred← citeshttps://doi.org/10.1016/s1571-0661(05)80002-7openalex-snapshot
Some Lessons from Using Static Analysis and Software Model Checking for Bug Finding
inferred← citeshttps://doi.org/10.1023/b:form.0000040029.73127.85openalex-snapshot
Lessons Learned from Model Checking a NASA Robot Controller
inferred← citeshttps://doi.org/10.1037/0000114-016openalex-snapshot
Where are we now, and where do we go from here?
inferred← citeshttps://doi.org/10.1109/access.2017.2685238openalex-snapshot
Applying Automated Model Extraction for Simulation and Verification of Real-Life SDL Specification With Spin
inferred← citeshttps://doi.org/10.1109/aero.2002.1036832openalex-snapshot
Using SPIN model checking for flight software verification
inferred← citeshttps://doi.org/10.1109/ahs.2006.68openalex-snapshot
SW-HW Co-design and Fault Tolerant Implementation for the LRID Wireless Communication System
inferred← citeshttps://doi.org/10.1109/ase.2001.989841openalex-snapshot
Automata-based verification of temporal properties on running programs
inferred← citeshttps://doi.org/10.1109/ase.2004.1342752openalex-snapshot
CHET: a system for checking dynamic specifications extended abstract
inferred← citeshttps://doi.org/10.1109/ase.2004.21openalex-snapshot
CHET: a system for checking dynamic specifications
inferred← citeshttps://doi.org/10.1109/ase.2006.60openalex-snapshot
Security Analysis of Crypto-based Java Programs using Automated Theorem Provers
inferred← citeshttps://doi.org/10.1109/cec.2008.4631354openalex-snapshot
Formality based genetic programming
inferred← citeshttps://doi.org/10.1109/cmpsac.2002.1045087openalex-snapshot
A tableau-based procedure for model checking programs
inferred← citeshttps://doi.org/10.1109/compsac.2008.143openalex-snapshot
Model Checking C Programs with Dynamic Memory Allocation
inferred← citeshttps://doi.org/10.1109/contel.2003.176918openalex-snapshot
Petri net modeling for reactive system verification
inferred← citeshttps://doi.org/10.1109/csci54926.2021.00361openalex-snapshot
Automatic Test Cases Generation for C Written Programs Using Model Checking
inferred← citeshttps://doi.org/10.1109/dsc53577.2021.00104openalex-snapshot
The Overview of SPIN in Software Model Checking
inferred← citeshttps://doi.org/10.1109/dsn-w50199.2020.00015openalex-snapshot
Online Verification through Model Checking of Medical Critical Intelligent Systems
inferred← citeshttps://doi.org/10.1109/dsn-w58399.2023.00069openalex-snapshot
Formalizing Model Inference of MicroPython
inferred← citeshttps://doi.org/10.1109/iccad.2005.1560083openalex-snapshot
Runtime integrity checking for inter-object connections
inferred← citeshttps://doi.org/10.1109/icieam.2018.8729118openalex-snapshot
On Use of Adaptive Schedules in Semantic Modeling of Real- Time Control Algorithms
inferred← citeshttps://doi.org/10.1109/icnp.2005.44openalex-snapshot
Typed Abstraction of Complex Network Compositions
inferred← citeshttps://doi.org/10.1109/icse.2000.870434openalex-snapshot
Bandera: extracting finite-state models from Java source code
inferred← citeshttps://doi.org/10.1109/icsm.2005.97openalex-snapshot
Understanding security goals provided by crypto-protocol implementations
inferred← citeshttps://doi.org/10.1109/icst.2012.81openalex-snapshot
X10X: Model Checking a New Programming Language with an "Old" Model Checker
inferred← citeshttps://doi.org/10.1109/ipdps.2003.1213510openalex-snapshot
Benchmark and framework for encouraging research on multi-threaded testing tools
inferred← citeshttps://doi.org/10.1109/irc.2019.00018openalex-snapshot
Static-Time Extraction and Analysis of the ROS Computation Graph
inferred← citeshttps://doi.org/10.1109/isca.2001.937448openalex-snapshot
A simple method for extracting models from protocol code
inferred← citeshttps://doi.org/10.1109/isola.2006.26openalex-snapshot
Implementing Influence Analysis Using Parameterised Boolean Equation Systems
inferred← citeshttps://doi.org/10.1109/isorc.2007.22openalex-snapshot
Automated Formal Verification and Testing of C Programs for Embedded Systems
inferred← citeshttps://doi.org/10.1109/issre.2016.47openalex-snapshot
Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus
inferred← citeshttps://doi.org/10.1109/memcod.2005.1487898openalex-snapshot
Verification of low-level crypto-protocol implementations using automated theorem proving
inferred← citeshttps://doi.org/10.1109/memcod.2014.6961844openalex-snapshot
A multi-core version of FreeRTOS verified for datarace and deadlock freedom
inferred← citeshttps://doi.org/10.1109/snpd.2007.363openalex-snapshot
State-based Time-Series Analysis and Prediction
inferred← citeshttps://doi.org/10.1109/tse.2023.3326056openalex-snapshot
Simulating Operational Memory Models Using Off-the-Shelf Program Analysis Tools
inferred← citeshttps://doi.org/10.1109/waimw.2006.29openalex-snapshot
Testing Path Generation Algorithm with Network Performance Constraints for Nondeterministic Parallel Programs
inferred← citeshttps://doi.org/10.1109/wises.2006.329116openalex-snapshot
Development of a Framework for Automated Systematic Testing of Safety-Critical Embedded Systems
inferred← citeshttps://doi.org/10.1142/s0218194020500242openalex-snapshot
Concurrent Bug Finding Based on Bounded Model Checking
inferred← citeshttps://doi.org/10.1145/1040305.1040314openalex-snapshot
Synthesis of interface specifications for Java classes
inferred← citeshttps://doi.org/10.1145/1069774.1069787openalex-snapshot
Trace effects and object orientation
inferred← citeshttps://doi.org/10.1145/1081180.1081184openalex-snapshot
Model checking software with well-defined APIs
inferred← citeshttps://doi.org/10.1145/1085130.1085133openalex-snapshot
Specifying and checking component usage
inferred← citeshttps://doi.org/10.1145/1101908.1101978openalex-snapshot
Code security analysis with assertions
inferred← citeshttps://doi.org/10.1145/1132960.1132962openalex-snapshot
Symmetry in temporal logic model checking
inferred← citeshttps://doi.org/10.1145/1217295.1217296openalex-snapshot
Foundations of incremental aspect model-checking
inferred← citeshttps://doi.org/10.1145/1459352.1459354openalex-snapshot
Using formal specifications to support testing
inferred← citeshttps://doi.org/10.1145/1570433.1570474openalex-snapshot
Contributing to safety and due diligence in safety-critical interactive systems development by generating and analyzing finite state models
inferred← citeshttps://doi.org/10.1145/2872362.2872364openalex-snapshot
How to Build Static Checking Systems Using Orders of Magnitude Less Code
inferred← citeshttps://doi.org/10.1145/3092282.3098206openalex-snapshot
The RERS 2017 challenge and workshop (invited paper)
inferred← citeshttps://doi.org/10.1145/337180.337364openalex-snapshot
Verification of time partitioning in the DEOS scheduler kernel
inferred← citeshttps://doi.org/10.1145/3425174.3425213openalex-snapshot
Asserting Functional Equivalence between C Code and SCADE Models in Code-to-Model Transformations
inferred← citeshttps://doi.org/10.1145/356989.356995openalex-snapshot
Using meta-level compilation to check FLASH protocol code
inferred← citeshttps://doi.org/10.1145/378993.379002openalex-snapshot
Using meta-level compilation to check FLASH protocol code
inferred← citeshttps://doi.org/10.1145/378995.379002openalex-snapshot
Using meta-level compilation to check FLASH protocol code
inferred← citeshttps://doi.org/10.1145/379240.379263openalex-snapshot
A simple method for extracting models for protocol code
inferred← citeshttps://doi.org/10.1145/384264.379002openalex-snapshot
Using meta-level compilation to check FLASH protocol code
inferred← citeshttps://doi.org/10.1145/384285.379263openalex-snapshot
A simple method for extracting models for protocol code
inferred← citeshttps://doi.org/10.1145/568760.568827openalex-snapshot
Local model checking of Java bytecode
inferred← citeshttps://doi.org/10.1145/958420.958424openalex-snapshot
Verifying linear time temporal logic properties of concurrent Ada programs with quasar
inferred← citeshttps://doi.org/10.1145/992211.958424openalex-snapshot
Verifying linear time temporal logic properties of concurrent Ada programs with quasar
inferred← citeshttps://doi.org/10.14279/tuj.eceasst.22.320openalex-snapshot
Tightly coupled verification of pervasive systems
inferred← citeshttps://doi.org/10.23919/ecc57647.2023.10178283openalex-snapshot
Formal Verification of a Controller Implementation in Fixed-Point Arithmetic
inferred← citeshttps://doi.org/10.3990/1.9789036515641openalex-snapshot
Towards effective model checking
inferred← citeshttps://doi.org/10.4028/www.scientific.net/amm.644-650.2342openalex-snapshot
A Case for Model Checking
inferred← citeshttps://doi.org/10.4028/www.scientific.net/amr.616-618.2055openalex-snapshot
Model Extraction and Reliability Verification on SOCKET Program
inferred← citeshttps://doi.org/10.53846/goediss-2464openalex-snapshot
Quality Assurance of Test Specifications for Reactive Systems
inferred← citeshttps://doi.org/10.5555/1251229.1251230openalex-snapshot
Checking system rules using system-specific, programmer-written compiler extensions
inferred← citeshttps://doi.org/10.5555/380921.380936openalex-snapshot
Behavioural analysis of the enterprise JavaBeans component architecture
inferred← citeshttps://doi.org/10.5772/33586openalex-snapshot
Software Reverse Engineering in the Domain of Complex Embedded Systems
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.