KLEE

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