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