Pages that link to "Item:Q5308405"

The following pages link to Tools and Algorithms for the Construction and Analysis of Systems (Q5308405):

Displaying 50 items.

• LCTD: test-guided proofs for C programs on LLVM (Q338629) (← links)
• Finding and fixing faults (Q414907) (← links)
• Symbolic predictive analysis for concurrent programs (Q432146) (← links)
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (Q457250) (← links)
• An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
• Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
• Budget-bounded model-checking pushdown systems (Q479843) (← links)
• The configurable SAT solver challenge (CSSC) (Q502389) (← links)
• SMT-based model checking for recursive programs (Q518396) (← links)
• Empirical software metrics for benchmarking of verification tools (Q526771) (← links)
• Doomed program points (Q633286) (← links)
• Under-approximating loops in C programs for fast counterexample detection (Q746774) (← links)
• Automatic analysis of DMA races using model checking and \(k\)-induction (Q763238) (← links)
• Quantifying software reliability via model-counting (Q832053) (← links)
• Verified cryptographic code for everybody (Q832216) (← links)
• Not all bugs are created equal, but robust reachability can tell the difference (Q832220) (← links)
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
• Why does Astrée scale up? (Q845249) (← links)
• Efficient SAT-based bounded model checking for software verification (Q947794) (← links)
• CPBPV: a constraint-programming framework for bounded program verification (Q968353) (← links)
• Data compression for proof replay (Q1040776) (← links)
• Lattice-based refinement in bounded model checking (Q1629959) (← links)
• A compiler for MSVL and its applications (Q1630985) (← links)
• VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
• Incremental bounded model checking for embedded software (Q1682291) (← links)
• On compiling Boolean circuits optimized for secure multi-party computation (Q1696583) (← links)
• A unifying view on SMT-based software verification (Q1703012) (← links)
• Sharpening constraint programming approaches for bit-vector theory (Q2011567) (← links)
• A formal methods approach to predicting new features of the eukaryotic vesicle traffic system (Q2022307) (← links)
• Efficient bounded model checking of heap-manipulating programs using tight field bounds (Q2044185) (← links)
• The \textsc{MergeSat} solver (Q2118329) (← links)
• Verification by gambling on program slices (Q2147204) (← links)
• Loop summarization using state and transition invariants (Q2248058) (← links)
• Scalable and precise refinement of cache timing analysis via path-sensitive verification (Q2251379) (← links)
• Automated formal synthesis of provably safe digital controllers for continuous plants (Q2303883) (← links)
• Abstract semantic diffing of evolving concurrent programs (Q2322311) (← links)
• System-level state equality detection for the formal dynamic verification of legacy distributed applications (Q2413022) (← links)
• A taxonomy of exact methods for partial Max-SAT (Q2434567) (← links)
• An automatic method for the dynamic construction of abstractions of states of a formal model (Q2452756) (← links)
• A compositional behavioral modeling framework for embedded system design and conformance checking (Q2506261) (← links)
• Embedded software verification using symbolic execution and uninterpreted functions (Q2506297) (← links)
• SATenstein: automatically building local search SAT solvers from components (Q2634473) (← links)
• CCA-Secure Keyed-Fully Homomorphic Encryption (Q2798772) (← links)
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
• Exploiting binary floating-point representations for constraint propagation (Q2806863) (← links)
• Context-Free Ambiguity Detection Using Multi-stack Pushdown Automata (Q2817371) (← links)
• Deciding Bit-Vector Formulas with mcSAT (Q2818018) (← links)
• Loop Invariant Symbolic Execution for Parallel Programs (Q2891433) (← links)
• Matching Multiplications in Bit-Vector Formulas (Q2961559) (← links)
• Partitioned Memory Models for Program Analysis (Q2961587) (← links)