Stem smt$ (all stems)

141 papers:

DAC-2015-LahiouelZT #smt #towards #using

Towards enhancing analog circuits sizing using SMT-based techniques (OL, MHZ, ST), p. 6.

DATE-2015-BiewerAGSH #approach #coordination #realtime #synthesis

A symbolic system synthesis approach for hard real-time systems based on coordinated SMT-solving (AB, BA, JG, TS, CH), pp. 357–362.

TACAS-2015-BjornerPF #named #optimisation #smt

νZ — An Optimizing SMT Solver (NB, ADP, LF), pp. 194–199.

TACAS-2015-ChistikovDM #approximate #estimation #probability #smt #source code

Approximate Counting in SMT and Value Estimation for Probabilistic Programs (DVC, RD, RM), pp. 320–334.

TACAS-2015-CimattiGMT #hybrid #model checking #named #smt

HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.

ICFP-2015-Pavlinovic0W #fault #locality #smt

Practical SMT-based type error localization (ZP, TK, TW), pp. 412–423.

CADE-2015-Baumgartner #named #proving #theorem proving

SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.

CADE-2015-ReynoldsB #data type #smt

A Decision Procedure for (Co)datatypes in SMT Solvers (AR, JCB), pp. 197–213.

CAV-2015-AbdullaACHRRS #constraints #named #smt #string

Norn: An SMT Solver for String Constraints (PAA, MFA, YFC, LH, AR, PR, JS), pp. 462–469.

CAV-2015-KonnovVW #abstraction #algorithm #distributed #model checking #smt

SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms (IK, HV, JW), pp. 85–102.

CAV-2015-ErezN #automation #bound #graph #smt #using

Finding Bounded Path in Graph Using SMT for Automatic Clock Routing (AE, AN), pp. 20–36.

CAV-2015-ReynoldsDKTB #quantifier #smt #synthesis

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.

CAV-2015-ZhuPJ #named #proving #smt

Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.

SAT-2015-CorziliusKJSA #c++ #named #open source #parallel #smt

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (FC, GK, SJ, SS, EÁ), pp. 360–368.

SAT-2015-HyvarinenMS #clustering #smt

Search-Space Partitioning for Parallelizing SMT Solvers (AEJH, MM, NS), pp. 369–386.

VMCAI-2015-ReynoldsK #induction #smt

Induction for SMT Solvers (AR, VK), pp. 80–98.

QoSA-2014-JohnsonC #architecture #evolution #performance #smt #specification

Efficient re-resolution of SMT specifications for evolving software architectures (KJ, RC), pp. 93–102.

DATE-2014-BiewerGH #novel #smt

A novel model for system-level decision making with combined ASP and SMT solving (AB, JG, CH), pp. 1–4.

DATE-2014-ErbSSB #fault #performance #smt

Efficient SMT-based ATPG for interconnect open defects (DE, KS, MS, BB), pp. 1–6.

FASE-2014-BersaniBGKP #smt

SMT-Based Checking of SOLOIST over Sparse Traces (MMB, DB, CG, SK, PSP), pp. 276–290.

TACAS-2014-EldibWS #smt #verification

SMT-Based Verification of Software Countermeasures against Side-Channel Attacks (HE, CW, PS), pp. 62–77.

WRLA-2014-RochaMM #analysis #smt

Rewriting Modulo SMT and Open System Analysis (CR, JM, CAM), pp. 247–262.

POPL-2014-LiAKGC #optimisation #smt

Symbolic optimization with SMT solvers (YL, AA, ZK, AG, MC), pp. 607–618.

FSE-2014-VakiliD #infinity #modelling #smt #using #verification

Verifying CTL-live properties of infinite state models using an SMT solver (AV, NAD), pp. 213–223.

ASPLOS-2014-EyermanE #concurrent #flexibility #manycore #parallel #smt #thread #towards

The benefit of SMT in the multi-core era: flexibility towards degrees of thread-level parallelism (SE, LE), pp. 591–606.

CAV-2014-EsparzaLMMN #analysis #approach #smt

An SMT-Based Approach to Coverability Analysis (JE, RLG, RM, PM, FN), pp. 603–619.

CAV-2014-KomuravelliGC #model checking #recursion #smt #source code

SMT-Based Model Checking for Recursive Programs (AK, AG, SC), pp. 17–34.

CAV-2014-LarrazNORR #proving #using

Proving Non-termination Using Max-SMT (DL, KN, AO, ERC, AR), pp. 779–796.

IJCAR-2014-BerdineB #refinement #smt

Computing All Implied Equalities via SMT-Based Partition Refinement (JB, NB), pp. 168–183.

SMT-2014-Barrett #named #question #smt

SMT: Where do we go from here? (CB), p. 1.

SMT-2014-BonichonDT #morphism #polymorphism

Extending SMT-LIB v2 with λ-Terms and Polymorphism (RB, DD, CT), pp. 53–62.

SMT-2014-FremontS #program analysis #smt

Speeding Up SMT-Based Quantitative Program Analysis (DJF, SAS), pp. 3–13.

SMT-2014-KhanhTO #difference #named #polynomial #smt

raSAT: SMT for Polynomial Inequality (TVK, VXT, MO), p. 67.

SMT-2014-KingBT #integer #linear #programming #smt

Leveraging Linear and Mixed Integer Programming for SMT (TK, CB, CT), p. 65.

TAP-2014-AminLR #smt

Computing with an SMT Solver (NA, KRML, TR), pp. 20–35.

ASE-2013-HuangMM #proving #smt #using

Proving MCAPI executions are correct using SMT (YH, EM, JM), pp. 26–36.

DATE-2013-BakshiH #reduction #smt #using

LFSR seed computation and reduction using SMT-based fault-chaining (DB, MSH), pp. 1071–1076.

DATE-2013-PigorschS #locality

Lemma localization: a practical method for downsizing SMT-interpolants (FP, CS), pp. 1405–1410.

TACAS-2013-CimattiGSS #smt

The MathSAT5 SMT Solver (AC, AG, BJS, RS), pp. 93–107.

TACAS-2013-HeizmannCDEHLNSP #contest

Ultimate Automizer with SMTInterpol — (Competition Contribution) (MH, JC, DD, EE, JH, ML, AN, CS, AP), pp. 641–643.

SEFM-2013-KeshishzadehMM #automation #debugging #detection #domain-specific language #fault #smt #using

Early Fault Detection in DSLs Using SMT Solving and Automated Debugging (SK, AJM, MRM), pp. 182–196.

KEOD-2013-NiewiadomskiP #ontology #smt #towards

Towards SMT-based Abstract Planning in PlanICS Ontology (AN, WP), pp. 123–131.

MoDELS-2013-SemerathHV #constraints #domain-specific language #graph #query #validation

Validation of Derived Features and Well-Formedness Constraints in DSLs — By Mapping Graph Queries to an SMT-Solver (OS, ÁH, DV), pp. 538–554.

MoDELS-2013-SemerathHV #constraints #domain-specific language #graph #query #validation

Validation of Derived Features and Well-Formedness Constraints in DSLs — By Mapping Graph Queries to an SMT-Solver (OS, ÁH, DV), pp. 538–554.

CADE-2013-GaoKC #named #smt

dReal: An SMT Solver for Nonlinear Theories over the Reals (SG, SK, EMC), pp. 208–214.

CADE-2013-ReynoldsTGKDB #finite #quantifier #smt

Quantifier Instantiation Techniques for Finite Model Finding in SMT (AR, CT, AG, SK, MD, CB), pp. 377–391.

CAV-2013-ChagantyLNR #learning #relational #smt #using

Combining Relational Learning with SMT Solvers Using CEGAR (ATC, AL, AVN, SKR), pp. 447–462.

CAV-2013-KomuravelliGCC #abstraction #automation #bound #model checking #smt

Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.

CAV-2013-PiskacWZ #automation #logic #smt #using

Automating Separation Logic Using SMT (RP, TW, DZ), pp. 773–789.

CAV-2013-ReynoldsTGK #finite #smt

Finite Model Finding in SMT (AR, CT, AG, SK), pp. 640–655.

CAV-2013-UhlerD #automation #named #query #smt #symbolic computation

Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries (RU, ND), pp. 678–683.

ICTSS-2013-Ibing #eclipse #execution #parallel #symbolic computation

Parallel SMT-Constrained Symbolic Execution for Eclipse CDT/Codan (AI), pp. 196–206.

VMCAI-2013-DehnertKP #bisimulation #markov #modelling #smt

SMT-Based Bisimulation Minimisation of Markov Models (CD, JPK, DP), pp. 28–47.

VMCAI-2013-LarrazRR #array #generative #invariant #smt

SMT-Based Array Invariant Generation (DL, ERC, AR), pp. 169–188.

ASE-2012-NijjarB #bound #smt #using #verification

Unbounded data model verification using SMT solvers (JN, TB), pp. 210–219.

DATE-2012-HuangBRBK #scheduling #smt

Static scheduling of a Time-Triggered Network-on-Chip based on SMT solving (JH, JOB, AR, CB, AK), pp. 509–514.

DATE-2012-SinghNL #generative #smt #testing

Hazard driven test generation for SMT processors (PS, VN, DLL), pp. 256–259.

MoDELS-2012-ButtnerEC #atl #off the shelf #on the #smt #using #verification

On Verifying ATL Transformations Using “off-the-shelf” SMT Solvers (FB, ME, JC), pp. 432–448.

MoDELS-2012-ButtnerEC #atl #off the shelf #on the #smt #using #verification

On Verifying ATL Transformations Using “off-the-shelf” SMT Solvers (FB, ME, JC), pp. 432–448.

FSE-2012-StoleeE #semantics #smt #towards

Toward semantic search via SMT solver (KTS, SGE), p. 25.

HPCA-2012-QianST #design #execution #named #smt

BulkSMT: Designing SMT processors for atomic-block execution (XQ, BS, JT), pp. 153–164.

CAV-2012-AlbertiBGRS #abstraction #array #named #smt

SAFARI: SMT-Based Abstraction for Arrays with Interpolants (FA, RB, SG, SR, NS), pp. 679–685.

CAV-2012-ConchonGKMZ #model checking #named #parallel #smt

Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems — Tool Paper (SC, AG, SK, AM, FZ), pp. 718–724.

CAV-2012-DilligDMA #smt

Minimum Satisfying Assignments for SMT (ID, TD, KLM, AA), pp. 394–409.

ICST-2012-DanH12a #c #mutation testing #named #semantics #testing #tool support

SMT-C: A Semantic Mutation Testing Tools for C (HD, RMH), pp. 654–663.

ICST-2012-LiuNT #bound #case study #smt #using #verification

Bounded Program Verification Using an SMT Solver: A Case Study (TL, MN, MT), pp. 101–110.

IJCAR-2012-Nieuwenhuis #challenge #satisfiability #smt

SAT and SMT Are Still Resolution: Questions and Challenges (RN), pp. 10–13.

IJCAR-2012-SebastianiT #cost analysis #optimisation #smt

Optimization in SMT with ℒ𝒜(ℚ) Cost Functions (RS, ST), pp. 484–498.

SAT-2012-CorziliusLJA #named

SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox — (Tool Presentation) (FC, UL, SJ, EÁ), pp. 442–448.

SAT-2012-ErmonLGSD #combinator

SMT-Aided Combinatorial Materials Discovery (SE, RL, CPG, BS, RBvD), pp. 172–185.

SMT-2012-AzizWD #estimation #machine learning #problem #smt

A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems (MAA, AGW, NMD), pp. 57–66.

SMT-2012-BjornerGMV #regular expression #sequence

SMT-LIB Sequences and Regular Expressions (NB, VG, RM, MV), pp. 77–87.

SMT-2012-CokGBD #contest #smt

The 2012 SMT Competition (DRC, AG, RB, MD), pp. 131–142.

SMT-2012-ConchonMRI #axiom #float #smt

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers (SC, GM, CR, MI), pp. 12–21.

SMT-2012-GoelKLT #smt #verification

SMT-Based System Verification with DVF (AG, SK, RL, MRT), pp. 32–43.

SMT-2012-MichelHGH #approach #automation #smt

An SMT-based approach to automated configuration (RM, AH, VG, PH), pp. 109–119.

SMT-2012-Shankar #architecture #smt

The Architecture of Inference from SMT to ETB (NS), p. 2.

VMCAI-2012-Leino #automation #induction #smt

Automating Induction with an SMT Solver (KRML), pp. 315–331.

ASE-2011-ArcainiGR #automation #generative #optimisation #satisfiability #smt #testing

Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions (PA, AG, ER), pp. 388–391.

DATE-2011-BradyHS

Counterexample-guided SMT-driven optimal buffer sizing (BAB, DEH, SAS), pp. 329–334.

DATE-2011-PavlenkoWSKDSG #algebra #named #problem #reasoning #smt #verification

STABLE: A new QF-BV SMT solver for hard verification problems combining Boolean reasoning with computer algebra (EP, MW, DS, WK, AD, FS, GMG), pp. 155–160.

ESOP-2011-GawlitzaM #smt

Improving Strategies via SMT Solving (TMG, DM), pp. 236–255.

FM-2011-GhaziT #reasoning #relational #smt

Relational Reasoning via SMT Solving (AAEG, MT), pp. 133–148.

ESEC-FSE-2011-PalmaST #interactive #requirements #smt #using

Using an SMT solver for interactive requirements prioritization (FP, AS, PT), pp. 48–58.

ICSE-2011-CordeiroF #bound #concurrent #model checking #multi #smt #thread #using #verification

Verifying multi-threaded software using smt-based context-bounded model checking (LC, BF), pp. 331–340.

CADE-2011-BlanchetteBP #smt

Extending Sledgehammer with SMT Solvers (JCB, SB, LCP), pp. 116–130.

CADE-2011-DeharbeFMP #problem #smt #symmetry

Exploiting Symmetry in SMT Problems (DD, PF, SM, BWP), pp. 222–236.

CADE-2011-HaarslevSV #automation #reasoning #smt

Automated Reasoning in 𝒜ℒ𝒞𝒬 via SMT (VH, RS, MV), pp. 283–298.

CADE-2011-KoksalKS #power of #programming #scala #smt

Scala to the Power of Z3: Integrating SMT and Programming (ASK, VK, PS), pp. 400–406.

CAV-2011-Lahiri #analysis #composition #smt

SMT-Based Modular Analysis of Sequential Systems Code (SKL), pp. 21–27.

TAP-2011-BentakoukPZ #behaviour #consistency #smt #testing #web #web service

Checking the Behavioral Conformance of Web Services with Symbolic Testing and an SMT Solver (LB, PP, FZ), pp. 33–50.

DATE-2010-CimattiFGKR #abstraction #integration #smt

Tighter integration of BDDs and SMT for Predicate Abstraction (AC, AF, AG, KK, MR), pp. 1707–1712.

DATE-2010-GellertPZFVS #architecture #design #energy #predict #smt

Energy-performance design space exploration in SMT architectures exploiting selective load value predictions (AG, GP, VZ, AF, LNV, CS), pp. 271–274.

TACAS-2010-BruttomessoPST

The OpenSMT Solver (RB, EP, NS, AT), pp. 150–153.

IFM-2010-FranzleTE #hybrid #probability #smt

Satisfaction Meets Expectations — Computing Expected Values of Probabilistic Hybrid Systems with SMT (MF, TT, AE), pp. 168–182.

SEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #smt #specification #verification

SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability (MMB, LC, AF, MP, MR), pp. 244–254.

ICFP-2010-BiermanGHL #semantics #smt #type system

Semantic subtyping with an SMT solver (GMB, ADG, CH, DEL), pp. 105–116.

FSE-2010-LiG #gpu #kernel #scalability #smt #verification

Scalable SMT-based verification of GPU kernel functions (GL, GG), pp. 187–196.

ICSE-2010-Cordeiro #bound #concurrent #embedded #model checking #multi #smt #thread

SMT-based bounded model checking for multi-threaded software in embedded systems (LC), pp. 373–376.

ASPLOS-2010-EyermanE #modelling #probability #scheduling #smt

Probabilistic job symbiosis modeling for SMT processor scheduling (SE, LE), pp. 91–102.

ICST-2010-JobstlWAW #consistency #execution #smt #symbolic computation #testing

When BDDs Fail: Conformance Testing with Symbolic Execution and SMT Solving (EJ, MW, BKA, FW), pp. 479–488.

SAT-2010-BofillSV #constraints #problem #smt

A System for Solving Constraint Satisfaction Problems with SMT (MB, JS, MV), pp. 300–305.

ASE-2009-CordeiroFM #bound #embedded #model checking #smt

SMT-Based Bounded Model Checking for Embedded ANSI-C Software (LCC, BF, JMS), pp. 137–148.

TACAS-2009-BrummayerB #array #named #performance #smt

Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays (RB, AB), pp. 174–177.

SAS-2009-Qadeer #algorithm #smt #using #verification

Algorithmic Verification of Systems Software Using SMT Solvers (SQ), p. 2.

SAC-2009-LeinoM #first-order #reasoning #smt

Reasoning about comprehensions with first-order SMT solvers (KRML, RM), pp. 615–622.

ASPLOS-2009-EyermanE #smt #thread

Per-thread cycle accounting in SMT processors (SE, LE), pp. 133–144.

CADE-2009-BoutonODF #named #performance

veriT: An Open, Trustable and Efficient SMT-Solver (TB, DCBdO, DD, PF), pp. 151–156.

CAV-2009-JhaLS #named #performance #smt

Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic (SJ, RL, SAS), pp. 668–674.

CAV-2009-LahiriQR #concurrent #detection #fault #precise #smt #using

Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers (SKL, SQ, ZR), pp. 509–524.

CAV-2009-SrivastavaGF #named #smt #verification

VS3: SMT Solvers for Program Verification (SS, SG, JSF), pp. 702–708.

CAV-2009-WintersteigerHM #approach #concurrent #smt

A Concurrent Portfolio Approach to SMT Solving (CMW, YH, LMdM), pp. 715–720.

TestCom-FATES-2009-GrieskampQWKC #constraints #interactive #smt #theorem proving

Interaction Coverage Meets Path Coverage by SMT Constraint Solving (WG, XQ, XW, NK, MBC), pp. 97–112.

DATE-2008-GanaiG #smt #source code

Completeness in SMT-based BMC for Software Programs (MKG, AG), pp. 831–836.

TACAS-2008-Moskal #proving #smt

Rocket-Fast Proof Checking for SMT Solvers (MM), pp. 486–500.

TACAS-2008-MouraB #named #performance #smt

Z3: An Efficient SMT Solver (LMdM, NB), pp. 337–340.

POPL-2008-LahiriQ #precise #smt #using #verification

Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.

HPCA-2008-RamirezPSV #performance #smt #thread

Runahead Threads to improve SMT performance (TR, AP, OJS, MV), pp. 149–158.

HPCA-2008-SubramaniamPL #dependence #memory management #named #predict #smt

PEEP: Exploiting predictability of memory dependences in SMT processors (SS, MP, GHL), pp. 137–148.

SMT-2007-BongioKLLM08 #encoding #first-order #proving #smt

Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.

CAV-2008-BofillNORR #smt

The Barcelogic SMT Solver (MB, RN, AO, ERC, AR), pp. 294–298.

CAV-2008-BruttomessoCFGS #smt

The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.

IJCAR-2008-GhilardiNRZ #model checking #smt #towards

Towards SMT Model Checking of Array-Based Systems (SG, EN, SR, DZ), pp. 67–82.

HPCA-2007-EyermanE #parallel #policy #smt

A Memory-Level Parallelism Aware Fetch Policy for SMT Processors (SE, LE), pp. 240–249.

CADE-2007-MouraB #performance #smt

Efficient E-Matching for SMT Solvers (LMdM, NB), pp. 183–198.

CAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt #verification

A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.

TACAS-2006-FontaineMMNT #automation #interactive #proving #smt #towards

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (PF, JYM, SM, LPN, AFT), pp. 167–181.

SAC-2006-Lo #protocol #smt

Data sharing protocols for SMT processors (SWL), pp. 891–895.

HPCA-2006-SharkeyP #performance #smt

Efficient instruction schedulers for SMT processors (JJS, DVP), pp. 288–298.

CAV-2006-LahiriNO #abstraction #performance #smt

SMT Techniques for Fast Predicate Abstraction (SKL, RN, AO), pp. 424–437.

CAV-2006-Roe #heuristic #modulo theories #proving #smt #theorem proving

The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.

SAT-2006-YuM #constraints #learning #linear #smt

Lemma Learning in SMT on Linear Constraints (YY, SM), pp. 142–155.

HPCA-2005-HasanJVB #smt

Heat Stroke: Power-Density-Based Denial of Service in SMT (JH, AJ, TNV, CEB), pp. 166–177.

HPCA-2005-LiBHS #architecture #energy #performance #smt

Performance, Energy, and Thermal Considerations for SMT and CMP Architectures (YL, DMB, ZH, KS), pp. 71–82.

HPCA-2005-ZhuZ #comparison #memory management #optimisation #performance #smt

A Performance Comparison of DRAM Memory System Optimizations for SMT Processors (ZZ, ZZ), pp. 213–224.

PPoPP-2005-JungLLH #adaptation #architecture #execution #multi #smt

Adaptive execution techniques for SMT multiprocessor architectures (CJ, DL, JL, SH), pp. 236–246.

CAV-2005-BarrettMS #contest #modulo theories #named #satisfiability

SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.

ASPLOS-2004-GomaaPV #named #operating system #smt

Heat-and-run: leveraging SMT and CMP to manage power density through the operating system (MAG, MDP, TNV), pp. 260–270.

HPCA-2003-El-MoursyA #performance #policy #smt

Front-End Policies for Improved Issue Efficiency in SMT Processors (AEM, DHA), pp. 31–40.

HPCA-2003-RedstoneEL #named #smt #thread

Mini-Threads: Increasing TLP on Small-Scale SMT Processors (JR, SJE, HML), pp. 19–30.

HPCA-2000-BurnsG #layout #question #smt

Quantifying the SMT Layout Overhead — Does SMT Pull Its Weight? (JB, JLG), pp. 109–120.