SIMPLIFY

From MaRDI portal
Revision as of 20:07, 5 March 2024 by Import240305080343 (talk | contribs) (Created automatically from import240305080343)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Software:17123



swMATH4976MaRDI QIDQ17123


No author found.





Related Items (only showing first 100 items - show all)

Ground interpolation for the theory of equalityPractical Realisation and Elimination of an ECC-Related Software Bug AttackAutomating Induction with an SMT SolverDecision Procedures for Region LogicDecision procedures for flat array propertiesInterpolation systems for ground proofs in automated deduction: a surveySemantically-guided goal-sensitive reasoning: model representationAdding decision procedures to SMT solvers using axioms with triggersQuantifier simplification by unification in SMTProduct programs in the wild: retrofitting program verifiers to check information flow securityTheory exploration powered by deductive synthesisVerification of SpecC using predicate abstractionEfficient weakest preconditionsAutomatic software model checking via constraint logicProving properties of functional programs by equality saturationA Lightweight Approach for Loop SummarizationSynthesis of positive logic programs for checking a class of definitions with infinite quantificationSearch-Space Partitioning for Parallelizing SMT SolversSAT-Based Model CheckingSatisfiability Modulo TheoriesCombining nonstably infinite theoriesTwo for the Price of One: Lifting Separation Logic AssertionsProgram verification with interacting analysis pluginsSpecification and verification challenges for sequential object-oriented programsAutomating regression verification of pointer programs by predicate abstractionBack to the futureHOL-Boogie -- an interactive prover-backend for the verifying C compilerStructured derivations: a unified proof style for teaching mathematicsUnnamed ItemSolving quantified linear arithmetic by counterexample-guided instantiationConstraint solving for finite model finding in SMT solversEquality detection for linear arithmetic constraintsVerifying Heap-Manipulating Programs in an SMT FrameworkThread Quantification for Concurrent Shape AnalysisAdapting Real Quantifier Elimination Methods for Conflict Set ComputationCounterexample-guided quantifier instantiation for synthesis in SMTAutomated verification of functional correctness of race-free GPU programsAutomated verification of shape, size and bag properties via user-defined predicates in separation logicOn deciding satisfiability by theorem proving with speculative inferencesAn instantiation scheme for satisfiability modulo theoriesA learning-based approach to synthesizing invariants for incomplete verification enginesFirst-order automated reasoning with theories: when deduction modulo theory meets practiceVerification conditions for source-level imperative programsModular Verification of Procedure Equivalence in the Presence of Memory AllocationSMELS: Satisfiability Modulo Equality with Lazy SuperpositionHOL-Boogie — An Interactive Prover for the Boogie Program-VerifierBounded Quantifier Instantiation for Checking Inductive InvariantsCounterexample-Guided Model SynthesisCongruence Closure with Free VariablesThe Daikon system for dynamic detection of likely invariantsA Polymorphic Intermediate Verification Language: Design and Logical EncodingFormal verification of a C-like memory model and its uses for verifying program transformationsCorrect Code Containing ContainersDecision procedures. An algorithmic point of viewUnnamed ItemExperience of improving the BLAST static verification toolUnnamed ItemFormal Proof of SCHUR Conjugate FunctionOne Logic to Use Them AllAutomatic decidability and combinabilityPredicate abstraction in a program logic calculusModular verification of multithreaded programsDescriptive and Relative Completeness of Logics for Higher-Order FunctionsGenerating error traces from verification-condition counterexamplesCertification Using the Mobius Base LogicPredicate Abstraction in a Program Logic CalculusRefutation-based synthesis in SMTEmbedded software verification using symbolic execution and uninterpreted functions${\mathcal{T}}$ -Decision by DecompositionDafny: An Automatic Program Verifier for Functional CorrectnessSatisfiability Solving and Model Generation for Quantified First-Order Logic FormulasComputing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear ConstraintsBeyond Quantifier-Free Interpolation in Extensions of Presburger ArithmeticUnnamed ItemCongruence Closure in Intensional Type TheorySolving Quantified Bit-Vector Formulas Using Binary Decision DiagramsOpenSMT2: An SMT Solver for Multi-core and Cloud ComputingInvariant based programming: Basic approach and teaching experiencesExtending SMT solvers to higher-order logicComplete Instantiation for Quantified Formulas in Satisfiabiliby Modulo TheoriesIncremental Instance Generation in Local ReasoningDon't care words with an application to the automata-based approach for real additionAbstract Counterexamples for Non-disjunctive AbstractionsModular SMT Proofs for Fast Reflexive Checking Inside CoqDelayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysisSolving quantified verification conditions using satisfiability modulo theoriesImproving Coq Propositional Reasoning Using a Lazy CNF Conversion SchemeUnification with abstraction and theory instantiation in saturation-based reasoningTheory decision by decompositionCombination of convex theories: modularity, deduction completeness, and explanationDCAS-based concurrent dequesSolving bitvectors with MCSAT: explanations from bits and piecesE-matching for Fun and ProfitModel-based Theory CombinationProgrammed Strategies for Program VerificationA posthumous contribution by Larry Wos: excerpts from an unpublished columnVerifying Whiley programs with BoogieSMELS: satisfiability modulo equality with lazy superpositionOn interpolation in automated theorem provingUnnamed Item


This page was built for software: SIMPLIFY