Linked e-resources
Details
Table of Contents
Witnessing Secure Compilation
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
Fixing Code That Explodes Under Symbolic Evaluation
The Correctness of a Code Generator for a Functional Language
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
A Systematic Approach to Abstract Interpretation of Program Transformations
Sharing ghost variables in a collection of abstract domains
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Synthesizing Environment Invariants for Modular Hardware Verification
Systematic Classi cation of Attackers via Bounded Model Checking
Cheap CTL Compassion in NuSMV
A Cooperative Parallelization Approach for Property-Directed k-Induction
Generalized Property-Directed Reachability for Hybrid Systems
Language Inclusion for Finite Prime Event Structures
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
Solving LIA* Using Approximations
Formalizing and checking Multilevel Consistency
Practical Abstractions for Automated Veri cation of Shared-Memory Concurrency
How to Win First-Order Safety Games
Improving Parity Game Solvers with Justifications.
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
Fixing Code That Explodes Under Symbolic Evaluation
The Correctness of a Code Generator for a Functional Language
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
A Systematic Approach to Abstract Interpretation of Program Transformations
Sharing ghost variables in a collection of abstract domains
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Synthesizing Environment Invariants for Modular Hardware Verification
Systematic Classi cation of Attackers via Bounded Model Checking
Cheap CTL Compassion in NuSMV
A Cooperative Parallelization Approach for Property-Directed k-Induction
Generalized Property-Directed Reachability for Hybrid Systems
Language Inclusion for Finite Prime Event Structures
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
Solving LIA* Using Approximations
Formalizing and checking Multilevel Consistency
Practical Abstractions for Automated Veri cation of Shared-Memory Concurrency
How to Win First-Order Safety Games
Improving Parity Game Solvers with Justifications.