Automatic detection of vulnerable variables for CTL properties of programs

DOI10.29007/DNPXMaRDI QIDQ7025196zbMATH OpenFDO

Authors Naïm Moussaoui Remil, C. Urban, Antoine Miné

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/DNPX

zbMATH Keywords

abstract interpretationCTLprogram verificationsecuritystatic analysis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• Abstract interpretation of CTL properties
• Conflict-driven conditional termination
• DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC
• Fairness modulo theory: a new approach to LTL software model checking
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Inference of ranking functions for proving temporal properties by abstract interpretation
• Not all bugs are created equal, but robust reachability can tell the difference
• Proving guarantee and recurrence temporal properties by abstract interpretation

This page was built for publication: Automatic detection of vulnerable variables for CTL properties of programs

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