KLEE
From MaRDI portal
Software:17045
swMATH4894MaRDI QIDQ17045FDOQ17045
Author name not available (Why is that?)
Cited In (39)
- Efficient strategies for CEGAR-based model checking
- Symbolic execution formally explained
- An Introduction to Test Specification in FQL
- Verifying Whiley programs with Boogie
- Constraint programming for dynamic symbolic execution of JavaScript
- Loop Invariant Symbolic Execution for Parallel Programs
- Wombit: a portfolio bit-vector solver using word-level propagation
- Algorithm selection for dynamic symbolic execution: a preliminary study
- Symbolic computation via program transformation
- Automation of Quantitative Information-Flow Analysis
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
- Symbolic Memory with Pointers
- Automated formal analysis and verification: an overview
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- LCTD: test-guided proofs for C programs on LLVM
- Sigma*
- Model checking boot code from AWS data centers
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Beginner's luck: a language for property-based generators
- Syntax-guided rewrite rule enumeration for SMT solvers
- Z3str2: an efficient solver for strings, regular expressions, and length constraints
- Efficient Loop Navigation for Symbolic Execution
- Rewriting modulo SMT and open system analysis
- Incremental bounded model checking for embedded software
- FEVS: a functional equivalence verification suite for high-performance scientific computing
- A Slice-Based Decision Procedure for Type-Based Partial Orders
- Combining Model Checking and Testing
- A generic framework for symbolic execution: a coinductive approach
- Harnessing static analysis to help learn pseudo-inverses of string manipulating procedures for automatic test generation
- Leveraging compiler intermediate representation for multi- and cross-language verification
- The configurable SAT solver challenge (CSSC)
- Executing and verifying higher-order functional-imperative programs in Maude
- Collective Assertions
- A sound and complete abstraction for reasoning about parallel prefix sums
- Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution
- TASS: the toolkit for accurate scientific software
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
This page was built for software: KLEE