swMATH26691MaRDI QIDQ38420FDOQ38420
Author name not available (Why is that?)
Official website: https://link.springer.com/chapter/10.1007%2F3-540-45937-5_16
Cited In (93)
- Compositional sequentialization of periodic programs
- Code2Inv
- Block-wise abstract interpretation by combining abstract domains with SMT
- Compositional Synthesis of Leakage Resilient Programs
- Rule-based static analysis of network protocol implementations
- Optimizing Pointer Analysis Using Bisimilarity
- Improving Generalization in Software IC3
- Stochastic modelling of communication protocols from source code
- Connecting program synthesis and reachability: automatic program repair using test-input generation
- \textsc{InterAspect}: aspect-oriented instrumentation with GCC
- High-fidelity C/C++ code transformation
- A formally verified compiler back-end
- Code2Inv: a deep learning framework for program verification
- Symbolic computation via program transformation
- Clang Static Analyzer
- Quantitative static analysis of communication protocols using abstract Markov chains
- Automated verification of functional correctness of race-free GPU programs
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Symbolic predictive analysis for concurrent programs
- Formal verification for C program
- Experience of improving the BLAST static verification tool
- Verification by gambling on program slices
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Adaptive locks: combining transactions and locks for efficient concurrency
- Limmat
- Eclat
- SANTE
- Continuation-passing C, compiling threads to events through continuations
- Generating C. System description
- UFO
- Atomizer
- Eraser
- Interproc
- CodeBoost
- SUIF
- Autolocker
- BER MetaOCaml
- Velodrome
- Cetus
- CBMC
- cminor
- SNZI
- CCured
- SingleTrack
- MOPS
- Feather-Trace
- Nighthawk
- CSIsat
- SPARK Pro
- TXL
- JCrasher
- AspectC++
- InterAspect
- PAGAI
- Sisal
- KLOVER
- MOP
- IKOS
- CodeSonar
- Klockwork
- EXPLODE
- Compiler-based attack origin tracking with dynamic taint analysis
- Proteus
- DDVerify
- LOCKSMITH
- BOXES
- OSMOSE
- Strymonas
- Jessie
- DyTa
- CHESS
- Kendo
- PhTM
- Terra
- Symbiotic 2
- Angelix
- jCUTE
- SymDIVINE
- Piton
- Ultimate Taipan
- Dytan
- Lwt
- UNITS
- Inferring effective types for static analysis of C programs
- Binutils
- CCCC
- Title not available (Why is that?)
- Strategies for scalable symbolic execution-driven test generation for programs
- A principled, complete, and efficient representation of C++
- CLN2INV
- Mechanized semantics for the clight subset of the C language
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
This page was built for software: CIL
