The following pages link to Programming Languages and Systems (Q5316581):
Displaying 37 items.
- ASTREE (Q25618) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Polynomial function intervals for floating-point software verification (Q457251) (← links)
- Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness (Q845242) (← links)
- Why does Astrée scale up? (Q845249) (← links)
- Proof-carrying code from certified abstract interpretation and fixpoint compression (Q860842) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- TASS: the toolkit for accurate scientific software (Q1949767) (← links)
- FEVS: a functional equivalence verification suite for high-performance scientific computing (Q1949768) (← links)
- Formal analysis of the compact position reporting algorithm (Q1996426) (← links)
- A decision tree lifted domain for analyzing program families with numerical features (Q2044175) (← links)
- Testing your (static analysis) truths (Q2119122) (← links)
- Fast and efficient bit-level precision tuning (Q2145313) (← links)
- Verified functional programming of an abstract interpreter (Q2145322) (← links)
- Verified compilation of floating-point computations (Q2352505) (← links)
- An approximation framework for solvers and decision procedures (Q2362497) (← links)
- System-level state equality detection for the formal dynamic verification of legacy distributed applications (Q2413022) (← links)
- A genetically modified Hoare logic (Q2422014) (← links)
- Abstract interpretation of microcontroller code: intervals meet congruences (Q2442953) (← links)
- Weakening additivity in adjoining closures (Q2520722) (← links)
- Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
- Splitting the Control Flow with Boolean Flags (Q3522080) (← links)
- A Scalable Segmented Decision Tree Abstract Domain (Q3587252) (← links)
- Abstract Interpretation of Symbolic Execution with Explicit State Updates (Q3638994) (← links)
- Polynomial Precise Interval Analysis Revisited (Q3644736) (← links)
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants (Q4913868) (← links)
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs (Q5041118) (← links)
- An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations (Q5170172) (← links)
- Structural Abstract Interpretation: A Formal Study Using Coq (Q5191090) (← links)
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (Q5206960) (← links)
- Building Certified Static Analysers by Modular Construction of Well-founded Lattices (Q5415621) (← links)
- An Improved Tight Closure Algorithm for Integer Octagonal Constraints (Q5452703) (← links)
- A Hybrid Denotational Semantics for Hybrid Systems (Q5458386) (← links)
- Transfer Function Synthesis without Quantifier Elimination (Q5892491) (← links)
- Parallel program analysis via range splitting (Q6535222) (← links)
- Adversarial reachability for program-level security analysis (Q6535227) (← links)
- Context-sensitive meta-constraint systems for explainable program analysis (Q6536146) (← links)
