BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
SMT
Satisfiability Modulo Theories
Google SMT

Tag #smt

163 papers:

CCCC-2020-PuriniBCB #analysis #image #pipes and filters #using
Bitwidth customization in image processing pipelines using interval analysis and SMT solvers (SP, VB, ZC, UB), pp. 167–178.
FMFM-2019-BardBD #fault #using
Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (JB, HB, ED), pp. 38–44.
ASPLOSASPLOS-2019-KondguliH #hardware #named #performance #thread #using
Bootstrapping: Using SMT Hardware to Improve Single-Thread Performance (SK, MH), pp. 687–700.
CASECASE-2019-HekmatnejadPF #scheduling #using
Task Scheduling with Nonlinear Costs using SMT Solvers (MH, GP, GF), pp. 183–188.
CASECASE-2019-RoselliBA #analysis #flexibility #problem #scheduling
SMT Solvers for Flexible Job-Shop Scheduling Problems: A Computational Analysis (SFR, KB, ), pp. 673–678.
ESOPESOP-2019-MartinezADGHHNP #automation #metaprogramming #proving
Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms (GM, DA, VD, NG, CH, CH, MN, ZP, CPC, JP, TR, AR, NS), pp. 30–59.
FASEFASE-2019-ZhangSMC #analysis #bound #constraints #scheduling #specification
SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language (MZ0, FS, FM, XC0), pp. 61–78.
CADECADE-2019-BarbosaROTB #higher-order #logic
Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.
CADECADE-2019-NiemetzPRZBT #independence #proving #towards
Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.
CAVCAV-2019-GavrilenkoLFHM #analysis #encoding #memory management #modelling
BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings (NG, HPdL, FF, KH, RM0), pp. 355–365.
CAVCAV-2019-JonasS #named #performance #quantifier
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (MJ, JS), pp. 64–73.
CAVCAV-2019-ReynoldsNBT #abstraction #constraints #string
High-Level Abstractions for Simplifying Extended String Constraints in SMT (AR, AN, CWB, CT), pp. 23–42.
FMFM-2018-Bjorner #industrial
Z3 and SMT in Industrial R&D (NB), pp. 675–678.
IFM-2018-DoughertyGR #analysis #protocol #security #using
Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA (DJD, JDG, JDR), pp. 130–150.
PADLPADL-2018-KringsLKHH #satisfiability
Three Is a Crowd: SAT, SMT and CLP on a Chessboard (SK, ML, PK, SH, MH), pp. 63–79.
POPLPOPL-2018-VazouTCSNWJ #refinement #verification
Refinement reflection: complete verification with SMT (NV, AT, VC, RGS, RRN, PW, RJ), p. 31.
ASEASE-2018-ChenH #control flow #verification
Control flow-guided SMT solving for program verification (JC, FH), pp. 351–361.
CASECASE-2018-GengenbachUAKRS #automation #component #flexibility #functional #workflow
An Integrated Workflow to Automatically Fabricate Flexible Electronics by Functional Printing and SMT Component Mounting (UG, MU, EA, LK, KMR, PS, VH), pp. 1624–1629.
CASECASE-2018-RoselliBA #comparison #evaluation #modelling #performance #problem #scheduling
SMT Solvers for Job-Shop Scheduling Problems: Models Comparison and Performance Evaluation (SFR, KB, ), pp. 547–552.
CAVCAV-2018-RobereKG #complexity #proving
The Proof Complexity of SMT Solvers (RR, AK, VG), pp. 275–293.
IFM-2017-BruschiPGLP #case study #model checking #protocol #verification
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study - (DB, ADP, SG, AL, EP), pp. 391–406.
IFM-2017-KovalovLGL #network #using
Task-Node Mapping in an Arbitrary Computer Network Using SMT Solver (AK, EL, AG, DL), pp. 177–191.
PPDPPPDP-2017-AguirreMPP #axiom
Conditional narrowing modulo SMT and axioms (LA, NMO, MP, IP), pp. 17–28.
CADECADE-2017-MengRTB #constraints #relational #theorem proving
Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.
CAVCAV-2017-KatzBDJK #named #network #performance #verification
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (GK, CWB, DLD, KJ, MJK), pp. 97–117.
CAVCAV-2017-ConchonIJMF #float #reasoning
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT (SC, MI, KJ, GM, CF), pp. 419–435.
CAVCAV-2017-EkiciMTKKRB #coq #named #plugin
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (BE, AM, CT, CK, GK, AR, CWB), pp. 126–133.
VMCAIVMCAI-2017-JiangCWW #abstract domain #abstract interpretation
Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT (JJ, LC, XW, JW0), pp. 310–329.
IFM-2016-KringsL #modelling #validation
SMT Solvers for Validation of B and Event-B Models (SK, ML), pp. 361–375.
SEFMSEFM-2016-ArcainiGR #automation #proving #refinement
SMT-Based Automatic Proof of ASM Model Refinement (PA, AG, ER), pp. 253–269.
MoDELSMoDELS-2016-PrzigodaWD #ocl #performance
Ground setting properties for an efficient translation of OCL in SMT-based model finding (NP, RW, RD), pp. 261–271.
OOPSLAOOPSLA-2016-WeitzWTEKT #protocol #scalability #verification
Scalable verification of border gateway protocol configurations with an SMT solver (KW, DW, ET, MDE, AK, ZT), pp. 765–780.
FSEFSE-2016-GurfinkelSM #verification
SMT-based verification of parameterized systems (AG, SS, YM), pp. 338–348.
CAVCAV-2016-KlenzeBH #flexibility #performance #synthesis
Fast, Flexible, and Minimal CTL Synthesis via SMT (TK, SB, AJH), pp. 136–156.
IJCARIJCAR-2016-BansalRBT #constraints #finite #set
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (KB, AR, CWB, CT), pp. 82–98.
IJCARIJCAR-2016-ReynoldsBCT #recursion
Model Finding for Recursive Functions in SMT (AR, JCB, SC, CT), pp. 133–151.
IJCARIJCAR-2016-TungKO #constraints #named #polynomial
raSAT: An SMT Solver for Polynomial Constraints (VXT, TVK, MO), pp. 228–237.
HaskellHaskell-2015-Diatchki #haskell
Improving Haskell types with SMT (ISD), pp. 1–10.
ICFPICFP-2015-Pavlinovic0W #fault #locality
Practical SMT-based type error localization (ZP, TK, TW), pp. 412–423.
DACDAC-2015-LahiouelZT #towards #using
Towards enhancing analog circuits sizing using SMT-based techniques (OL, MHZ, ST), p. 6.
TACASTACAS-2015-BjornerPF #named #optimisation
νZ — An Optimizing SMT Solver (NB, ADP, LF), pp. 194–199.
TACASTACAS-2015-ChistikovDM #approximate #estimation #probability #source code
Approximate Counting in SMT and Value Estimation for Probabilistic Programs (DVC, RD, RM), pp. 320–334.
TACASTACAS-2015-CimattiGMT #hybrid #model checking #named
HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.
CADECADE-2015-ReynoldsB #data type
A Decision Procedure for (Co)datatypes in SMT Solvers (AR, JCB), pp. 197–213.
CAVCAV-2015-AbdullaACHRRS #constraints #named #string
Norn: An SMT Solver for String Constraints (PAA, MFA, YFC, LH, AR, PR, JS), pp. 462–469.
CAVCAV-2015-KonnovVW #abstraction #algorithm #distributed #model checking
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms (IK, HV, JW), pp. 85–102.
CAVCAV-2015-ErezN #automation #bound #graph #using
Finding Bounded Path in Graph Using SMT for Automatic Clock Routing (AE, AN), pp. 20–36.
CAVCAV-2015-ReynoldsDKTB #quantifier #synthesis
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT (AR, MD, VK, CT, CWB), pp. 198–216.
CAVCAV-2015-ZhuPJ #named #proving
Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.
ICSTSAT-2015-CorziliusKJSA #c++ #named #open source #parallel
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (FC, GK, SJ, SS, ), pp. 360–368.
ICSTSAT-2015-HyvarinenMS #clustering
Search-Space Partitioning for Parallelizing SMT Solvers (AEJH, MM, NS), pp. 369–386.
VMCAIVMCAI-2015-ReynoldsK #induction
Induction for SMT Solvers (AR, VK), pp. 80–98.
QoSAQoSA-2014-JohnsonC #architecture #evolution #performance #specification
Efficient re-resolution of SMT specifications for evolving software architectures (KJ, RC), pp. 93–102.
POPLPOPL-2014-LiAKGC #optimisation
Symbolic optimization with SMT solvers (YL, AA, ZK, AG, MC), pp. 607–618.
FSEFSE-2014-VakiliD #infinity #modelling #using #verification
Verifying CTL-live properties of infinite state models using an SMT solver (AV, NAD), pp. 213–223.
ASPLOSASPLOS-2014-EyermanE #concurrent #flexibility #manycore #parallel #thread #towards
The benefit of SMT in the multi-core era: flexibility towards degrees of thread-level parallelism (SE, LE), pp. 591–606.
DATEDATE-2014-BiewerGH #novel
A novel model for system-level decision making with combined ASP and SMT solving (AB, JG, CH), pp. 1–4.
DATEDATE-2014-ErbSSB #fault #performance
Efficient SMT-based ATPG for interconnect open defects (DE, KS, MS, BB), pp. 1–6.
FASEFASE-2014-BersaniBGKP
SMT-Based Checking of SOLOIST over Sparse Traces (MMB, DB, CG, SK, PSP), pp. 276–290.
TACASTACAS-2014-EldibWS #verification
SMT-Based Verification of Software Countermeasures against Side-Channel Attacks (HE, CW, PS), pp. 62–77.
WRLAWRLA-2014-RochaMM #analysis
Rewriting Modulo SMT and Open System Analysis (CR, JM, CAM), pp. 247–262.
CAVCAV-2014-EsparzaLMMN #analysis #approach
An SMT-Based Approach to Coverability Analysis (JE, RLG, RM, PM, FN), pp. 603–619.
CAVCAV-2014-KomuravelliGC #model checking #recursion #source code
SMT-Based Model Checking for Recursive Programs (AK, AG, SC), pp. 17–34.
IJCARIJCAR-2014-BerdineB #refinement
Computing All Implied Equalities via SMT-Based Partition Refinement (JB, NB), pp. 168–183.
SMTSMT-2014-Barrett #named #question
SMT: Where do we go from here? (CB), p. 1.
SMTSMT-2014-FremontS #program analysis
Speeding Up SMT-Based Quantitative Program Analysis (DJF, SAS), pp. 3–13.
SMTSMT-2014-KhanhTO #difference #named #polynomial
raSAT: SMT for Polynomial Inequality (TVK, VXT, MO), p. 67.
SMTSMT-2014-KingBT #integer #linear #programming
Leveraging Linear and Mixed Integer Programming for SMT (TK, CB, CT), p. 65.
TAPTAP-2014-AminLR
Computing with an SMT Solver (NA, KRML, TR), pp. 20–35.
SEFMSEFM-2013-KeshishzadehMM #automation #debugging #detection #domain-specific language #fault #using
Early Fault Detection in DSLs Using SMT Solving and Automated Debugging (SK, AJM, MRM), pp. 182–196.
KEODKEOD-2013-NiewiadomskiP #ontology #towards
Towards SMT-based Abstract Planning in PlanICS Ontology (AN, WP), pp. 123–131.
ASEASE-2013-HuangMM #proving #using
Proving MCAPI executions are correct using SMT (YH, EM, JM), pp. 26–36.
DATEDATE-2013-BakshiH #reduction #using
LFSR seed computation and reduction using SMT-based fault-chaining (DB, MSH), pp. 1071–1076.
TACASTACAS-2013-CimattiGSS
The MathSAT5 SMT Solver (AC, AG, BJS, RS), pp. 93–107.
CADECADE-2013-GaoKC #named
dReal: An SMT Solver for Nonlinear Theories over the Reals (SG, SK, EMC), pp. 208–214.
CADECADE-2013-ReynoldsTGKDB #finite #quantifier
Quantifier Instantiation Techniques for Finite Model Finding in SMT (AR, CT, AG, SK, MD, CB), pp. 377–391.
CAVCAV-2013-ChagantyLNR #learning #relational #using
Combining Relational Learning with SMT Solvers Using CEGAR (ATC, AL, AVN, SKR), pp. 447–462.
CAVCAV-2013-KomuravelliGCC #abstraction #automation #bound #model checking
Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.
CAVCAV-2013-PiskacWZ #automation #logic #using
Automating Separation Logic Using SMT (RP, TW, DZ), pp. 773–789.
CAVCAV-2013-ReynoldsTGK #finite
Finite Model Finding in SMT (AR, CT, AG, SK), pp. 640–655.
CAVCAV-2013-UhlerD #automation #named #query #symbolic computation
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries (RU, ND), pp. 678–683.
VMCAIVMCAI-2013-DehnertKP #bisimulation #markov #modelling
SMT-Based Bisimulation Minimisation of Markov Models (CD, JPK, DP), pp. 28–47.
VMCAIVMCAI-2013-LarrazRR #array #generative #invariant
SMT-Based Array Invariant Generation (DL, ERC, AR), pp. 169–188.
MODELSMoDELS-2012-ButtnerEC #atl #off the shelf #on the #using #verification
On Verifying ATL Transformations Using “off-the-shelf” SMT Solvers (FB, ME, JC), pp. 432–448.
ASEASE-2012-NijjarB #bound #using #verification
Unbounded data model verification using SMT solvers (JN, TB), pp. 210–219.
FSEFSE-2012-StoleeE #semantics #towards
Toward semantic search via SMT solver (KTS, SGE), p. 25.
DATEDATE-2012-HuangBRBK #scheduling
Static scheduling of a Time-Triggered Network-on-Chip based on SMT solving (JH, JOB, AR, CB, AK), pp. 509–514.
DATEDATE-2012-SinghNL #generative #testing
Hazard driven test generation for SMT processors (PS, VN, DLL), pp. 256–259.
HPCAHPCA-2012-QianST #design #execution #named
BulkSMT: Designing SMT processors for atomic-block execution (XQ, BS, JT), pp. 153–164.
CAVCAV-2012-AlbertiBGRS #abstraction #array #named
SAFARI: SMT-Based Abstraction for Arrays with Interpolants (FA, RB, SG, SR, NS), pp. 679–685.
CAVCAV-2012-ConchonGKMZ #model checking #named #parallel
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems — Tool Paper (SC, AG, SK, AM, FZ), pp. 718–724.
CAVCAV-2012-DilligDMA
Minimum Satisfying Assignments for SMT (ID, TD, KLM, AA), pp. 394–409.
ICSTICST-2012-LiuNT #bound #case study #using #verification
Bounded Program Verification Using an SMT Solver: A Case Study (TL, MN, MT), pp. 101–110.
IJCARIJCAR-2012-Nieuwenhuis #challenge #satisfiability
SAT and SMT Are Still Resolution: Questions and Challenges (RN), pp. 10–13.
IJCARIJCAR-2012-SebastianiT #cost analysis #optimisation
Optimization in SMT with ℒ𝒜(ℚ) Cost Functions (RS, ST), pp. 484–498.
SMTSMT-2012-AzizWD #estimation #machine learning #problem
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems (MAA, AGW, NMD), pp. 57–66.
SMTSMT-2012-CokGBD #contest
The 2012 SMT Competition (DRC, AG, RB, MD), pp. 131–142.
SMTSMT-2012-ConchonMRI #axiom #float
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers (SC, GM, CR, MI), pp. 12–21.
SMTSMT-2012-GoelKLT #verification
SMT-Based System Verification with DVF (AG, SK, RL, MRT), pp. 32–43.
SMTSMT-2012-MichelHGH #approach #automation
An SMT-based approach to automated configuration (RM, AH, VG, PH), pp. 109–119.
SMTSMT-2012-Shankar #architecture
The Architecture of Inference from SMT to ETB (NS), p. 2.
VMCAIVMCAI-2012-Leino #automation #induction
Automating Induction with an SMT Solver (KRML), pp. 315–331.
FMFM-2011-GhaziT #reasoning #relational
Relational Reasoning via SMT Solving (AAEG, MT), pp. 133–148.
ASEASE-2011-ArcainiGR #automation #generative #optimisation #satisfiability #testing
Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions (PA, AG, ER), pp. 388–391.
ESEC-FSEESEC-FSE-2011-PalmaST #interactive #requirements #using
Using an SMT solver for interactive requirements prioritization (FP, AS, PT), pp. 48–58.
ICSEICSE-2011-CordeiroF #bound #concurrent #model checking #multi #thread #using #verification
Verifying multi-threaded software using smt-based context-bounded model checking (LC, BF), pp. 331–340.
DATEDATE-2011-PavlenkoWSKDSG #algebra #named #problem #reasoning #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.
ESOPESOP-2011-GawlitzaM
Improving Strategies via SMT Solving (TMG, DM), pp. 236–255.
CADECADE-2011-BlanchetteBP
Extending Sledgehammer with SMT Solvers (JCB, SB, LCP), pp. 116–130.
CADECADE-2011-DeharbeFMP #problem #symmetry
Exploiting Symmetry in SMT Problems (DD, PF, SM, BWP), pp. 222–236.
CADECADE-2011-HaarslevSV #automation #reasoning
Automated Reasoning in 𝒜ℒ𝒞𝒬 via SMT (VH, RS, MV), pp. 283–298.
CADECADE-2011-KoksalKS #power of #programming #scala
Scala to the Power of Z3: Integrating SMT and Programming (ASK, VK, PS), pp. 400–406.
CAVCAV-2011-Lahiri #analysis #composition
SMT-Based Modular Analysis of Sequential Systems Code (SKL), pp. 21–27.
TAPTAP-2011-BentakoukPZ #behaviour #consistency #testing #web #web service
Checking the Behavioral Conformance of Web Services with Symbolic Testing and an SMT Solver (LB, PP, FZ), pp. 33–50.
IFMIFM-2010-FranzleTE #hybrid #probability
Satisfaction Meets Expectations — Computing Expected Values of Probabilistic Hybrid Systems with SMT (MF, TT, AE), pp. 168–182.
SEFMSEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #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.
ICFPICFP-2010-BiermanGHL #semantics #type system
Semantic subtyping with an SMT solver (GMB, ADG, CH, DEL), pp. 105–116.
FSEFSE-2010-LiG #gpu #kernel #scalability #verification
Scalable SMT-based verification of GPU kernel functions (GL, GG), pp. 187–196.
ICSEICSE-2010-Cordeiro #bound #concurrent #embedded #model checking #multi #thread
SMT-based bounded model checking for multi-threaded software in embedded systems (LC), pp. 373–376.
ASPLOSASPLOS-2010-EyermanE #modelling #probability #scheduling
Probabilistic job symbiosis modeling for SMT processor scheduling (SE, LE), pp. 91–102.
DATEDATE-2010-CimattiFGKR #abstraction #integration
Tighter integration of BDDs and SMT for Predicate Abstraction (AC, AF, AG, KK, MR), pp. 1707–1712.
DATEDATE-2010-GellertPZFVS #architecture #design #energy #predict
Energy-performance design space exploration in SMT architectures exploiting selective load value predictions (AG, GP, VZ, AF, LNV, CS), pp. 271–274.
ICSTICST-2010-JobstlWAW #consistency #execution #symbolic computation #testing
When BDDs Fail: Conformance Testing with Symbolic Execution and SMT Solving (EJ, MW, BKA, FW), pp. 479–488.
ICSTSAT-2010-BofillSV #constraints #problem
A System for Solving Constraint Satisfaction Problems with SMT (MB, JS, MV), pp. 300–305.
SASSAS-2009-Qadeer #algorithm #using #verification
Algorithmic Verification of Systems Software Using SMT Solvers (SQ), p. 2.
ASEASE-2009-CordeiroFM #bound #embedded #model checking
SMT-Based Bounded Model Checking for Embedded ANSI-C Software (LCC, BF, JMS), pp. 137–148.
SACSAC-2009-LeinoM #first-order #reasoning
Reasoning about comprehensions with first-order SMT solvers (KRML, RM), pp. 615–622.
ASPLOSASPLOS-2009-EyermanE #thread
Per-thread cycle accounting in SMT processors (SE, LE), pp. 133–144.
TACASTACAS-2009-BrummayerB #array #named #performance
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays (RB, AB), pp. 174–177.
CAVCAV-2009-JhaLS #named #performance
Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic (SJ, RL, SAS), pp. 668–674.
CAVCAV-2009-LahiriQR #concurrent #detection #fault #precise #using
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers (SKL, SQ, ZR), pp. 509–524.
CAVCAV-2009-SrivastavaGF #named #verification
VS3: SMT Solvers for Program Verification (SS, SG, JSF), pp. 702–708.
CAVCAV-2009-WintersteigerHM #approach #concurrent
A Concurrent Portfolio Approach to SMT Solving (CMW, YH, LMdM), pp. 715–720.
FATESTestCom-FATES-2009-GrieskampQWKC #constraints #interactive #theorem proving
Interaction Coverage Meets Path Coverage by SMT Constraint Solving (WG, XQ, XW, NK, MBC), pp. 97–112.
POPLPOPL-2008-LahiriQ #precise #using #verification
Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.
DATEDATE-2008-GanaiG #source code
Completeness in SMT-based BMC for Software Programs (MKG, AG), pp. 831–836.
HPCAHPCA-2008-RamirezPSV #performance #thread
Runahead Threads to improve SMT performance (TR, AP, OJS, MV), pp. 149–158.
HPCAHPCA-2008-SubramaniamPL #dependence #memory management #named #predict
PEEP: Exploiting predictability of memory dependences in SMT processors (SS, MP, GHL), pp. 137–148.
TACASTACAS-2008-Moskal #proving
Rocket-Fast Proof Checking for SMT Solvers (MM), pp. 486–500.
TACASTACAS-2008-MouraB #named #performance
Z3: An Efficient SMT Solver (LMdM, NB), pp. 337–340.
SMTSMT-2007-BongioKLLM08 #encoding #first-order #proving
Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.
CAVCAV-2008-BofillNORR
The Barcelogic SMT Solver (MB, RN, AO, ERC, AR), pp. 294–298.
CAVCAV-2008-BruttomessoCFGS
The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.
IJCARIJCAR-2008-GhilardiNRZ #model checking #towards
Towards SMT Model Checking of Array-Based Systems (SG, EN, SR, DZ), pp. 67–82.
HPCAHPCA-2007-EyermanE #parallel #policy
A Memory-Level Parallelism Aware Fetch Policy for SMT Processors (SE, LE), pp. 240–249.
CADECADE-2007-MouraB #performance
Efficient E-Matching for SMT Solvers (LMdM, NB), pp. 183–198.
CAVCAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #verification
A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.
SACSAC-2006-Lo #protocol
Data sharing protocols for SMT processors (SWL), pp. 891–895.
HPCAHPCA-2006-SharkeyP #performance
Efficient instruction schedulers for SMT processors (JJS, DVP), pp. 288–298.
TACASTACAS-2006-FontaineMMNT #automation #interactive #proving #towards
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (PF, JYM, SM, LPN, AFT), pp. 167–181.
CAVCAV-2006-LahiriNO #abstraction #performance
SMT Techniques for Fast Predicate Abstraction (SKL, RN, AO), pp. 424–437.
CAVCAV-2006-Roe #heuristic #modulo theories #proving #theorem proving
The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
ICSTSAT-2006-YuM #constraints #learning #linear
Lemma Learning in SMT on Linear Constraints (YY, SM), pp. 142–155.
HPCAHPCA-2005-HasanJVB
Heat Stroke: Power-Density-Based Denial of Service in SMT (JH, AJ, TNV, CEB), pp. 166–177.
HPCAHPCA-2005-LiBHS #architecture #energy #performance
Performance, Energy, and Thermal Considerations for SMT and CMP Architectures (YL, DMB, ZH, KS), pp. 71–82.
HPCAHPCA-2005-ZhuZ #comparison #memory management #optimisation #performance
A Performance Comparison of DRAM Memory System Optimizations for SMT Processors (ZZ, ZZ), pp. 213–224.
PPoPPPPoPP-2005-JungLLH #adaptation #architecture #execution #multi
Adaptive execution techniques for SMT multiprocessor architectures (CJ, DL, JL, SH), pp. 236–246.
ASPLOSASPLOS-2004-GomaaPV #named #operating system
Heat-and-run: leveraging SMT and CMP to manage power density through the operating system (MAG, MDP, TNV), pp. 260–270.
HPCAHPCA-2003-El-MoursyA #performance #policy
Front-End Policies for Improved Issue Efficiency in SMT Processors (AEM, DHA), pp. 31–40.
HPCAHPCA-2003-RedstoneEL #named #thread
Mini-Threads: Increasing TLP on Small-Scale SMT Processors (JR, SJE, HML), pp. 19–30.
PDPPDP-2002-GoncalvesN #performance #process #scheduling
Improving SMT Performance Scheduling Processes (RG, POAN), pp. 327–334.
PDPPDP-2001-GoncalvesPPSNS #architecture #branch #performance #predict
Evaluating the Effects of Branch Prediction Accuracy on the Performance of SMT Architectures (RG, MLP, GDP, TGSdS, POAN, RS), pp. 355–362.
HPCAHPCA-2000-BurnsG #layout #question
Quantifying the SMT Layout Overhead — Does SMT Pull Its Weight? (JB, JLG), pp. 109–120.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.