SMT
Satisfiability Modulo Theories

---

SMT

Tag #smt

163 papers:

CC-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.

FM-2019-BardBD #fault #using

Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (JB, HB, ED), pp. 38–44.

ASPLOS-2019-KondguliH #hardware #named #performance #thread #using

Bootstrapping: Using SMT Hardware to Improve Single-Thread Performance (SK, MH), pp. 687–700.

CASE-2019-HekmatnejadPF #scheduling #using

Task Scheduling with Nonlinear Costs using SMT Solvers (MH, GP, GF), pp. 183–188.

CASE-2019-RoselliBA #analysis #flexibility #problem #scheduling

SMT Solvers for Flexible Job-Shop Scheduling Problems: A Computational Analysis (SFR, KB, KÅ), pp. 673–678.

ESOP-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.

FASE-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.

CADE-2019-BarbosaROTB #higher-order #logic

Extending SMT Solvers to Higher-Order Logic (HB, AR, DEO, CT, CWB), pp. 35–54.

CADE-2019-NiemetzPRZBT #independence #proving #towards

Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.

CAV-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.

CAV-2019-JonasS #named #performance #quantifier

Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (MJ, JS), pp. 64–73.

CAV-2019-ReynoldsNBT #abstraction #constraints #string

High-Level Abstractions for Simplifying Extended String Constraints in SMT (AR, AN, CWB, CT), pp. 23–42.

FM-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.

PADL-2018-KringsLKHH #satisfiability

Three Is a Crowd: SAT, SMT and CLP on a Chessboard (SK, ML, PK, SH, MH), pp. 63–79.

POPL-2018-VazouTCSNWJ #refinement #verification

Refinement reflection: complete verification with SMT (NV, AT, VC, RGS, RRN, PW, RJ), p. 31.

ASE-2018-ChenH #control flow #verification

Control flow-guided SMT solving for program verification (JC, FH), pp. 351–361.

CASE-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.

CASE-2018-RoselliBA #comparison #evaluation #modelling #performance #problem #scheduling

SMT Solvers for Job-Shop Scheduling Problems: Models Comparison and Performance Evaluation (SFR, KB, KÅ), pp. 547–552.

CAV-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.

PPDP-2017-AguirreMPP #axiom

Conditional narrowing modulo SMT and axioms (LA, NMO, MP, IP), pp. 17–28.

CADE-2017-MengRTB #constraints #relational #theorem proving

Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.

CAV-2017-KatzBDJK #named #network #performance #verification

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (GK, CWB, DLD, KJ, MJK), pp. 97–117.

CAV-2017-ConchonIJMF #float #reasoning

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT (SC, MI, KJ, GM, CF), pp. 419–435.

CAV-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.

VMCAI-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.

SEFM-2016-ArcainiGR #automation #proving #refinement

SMT-Based Automatic Proof of ASM Model Refinement (PA, AG, ER), pp. 253–269.

MoDELS-2016-PrzigodaWD #ocl #performance

Ground setting properties for an efficient translation of OCL in SMT-based model finding (NP, RW, RD), pp. 261–271.

OOPSLA-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.

FSE-2016-GurfinkelSM #verification

SMT-based verification of parameterized systems (AG, SS, YM), pp. 338–348.

CAV-2016-KlenzeBH #flexibility #performance #synthesis

Fast, Flexible, and Minimal CTL Synthesis via SMT (TK, SB, AJH), pp. 136–156.

IJCAR-2016-BansalRBT #constraints #finite #set

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (KB, AR, CWB, CT), pp. 82–98.

IJCAR-2016-ReynoldsBCT #recursion

Model Finding for Recursive Functions in SMT (AR, JCB, SC, CT), pp. 133–151.

IJCAR-2016-TungKO #constraints #named #polynomial

raSAT: An SMT Solver for Polynomial Constraints (VXT, TVK, MO), pp. 228–237.

Haskell-2015-Diatchki #haskell

Improving Haskell types with SMT (ISD), pp. 1–10.

ICFP-2015-Pavlinovic0W #fault #locality

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

DAC-2015-LahiouelZT #towards #using

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

TACAS-2015-BjornerPF #named #optimisation

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

TACAS-2015-ChistikovDM #approximate #estimation #probability #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

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

CADE-2015-ReynoldsB #data type

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

CAV-2015-AbdullaACHRRS #constraints #named #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 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 #using

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

CAV-2015-ReynoldsDKTB #quantifier #synthesis

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

CAV-2015-ZhuPJ #named #proving

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

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

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

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

VMCAI-2015-ReynoldsK #induction

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

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

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

POPL-2014-LiAKGC #optimisation

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

FSE-2014-VakiliD #infinity #modelling #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 #thread #towards

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

DATE-2014-BiewerGH #novel

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

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

FASE-2014-BersaniBGKP

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

TACAS-2014-EldibWS #verification

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

WRLA-2014-RochaMM #analysis

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

CAV-2014-EsparzaLMMN #analysis #approach

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

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

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

IJCAR-2014-BerdineB #refinement

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

SMT-2014-Barrett #named #question

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

SMT-2014-FremontS #program analysis

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

SMT-2014-KhanhTO #difference #named #polynomial

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

SMT-2014-KingBT #integer #linear #programming

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

TAP-2014-AminLR

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

SEFM-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.

KEOD-2013-NiewiadomskiP #ontology #towards

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

ASE-2013-HuangMM #proving #using

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

DATE-2013-BakshiH #reduction #using

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

TACAS-2013-CimattiGSS

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

CADE-2013-GaoKC #named

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

CADE-2013-ReynoldsTGKDB #finite #quantifier

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

CAV-2013-ChagantyLNR #learning #relational #using

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

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

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

CAV-2013-PiskacWZ #automation #logic #using

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

CAV-2013-ReynoldsTGK #finite

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

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

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

VMCAI-2013-DehnertKP #bisimulation #markov #modelling

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

VMCAI-2013-LarrazRR #array #generative #invariant

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

MoDELS-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.

ASE-2012-NijjarB #bound #using #verification

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

FSE-2012-StoleeE #semantics #towards

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

DATE-2012-HuangBRBK #scheduling

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 #testing

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

HPCA-2012-QianST #design #execution #named

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

CAV-2012-AlbertiBGRS #abstraction #array #named

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

CAV-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.

CAV-2012-DilligDMA

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

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

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

IJCAR-2012-Nieuwenhuis #challenge #satisfiability

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

IJCAR-2012-SebastianiT #cost analysis #optimisation

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

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

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

SMT-2012-CokGBD #contest

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

SMT-2012-ConchonMRI #axiom #float

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

SMT-2012-GoelKLT #verification

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

SMT-2012-MichelHGH #approach #automation

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

SMT-2012-Shankar #architecture

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

VMCAI-2012-Leino #automation #induction

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

FM-2011-GhaziT #reasoning #relational

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

ASE-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-FSE-2011-PalmaST #interactive #requirements #using

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

ICSE-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.

DATE-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.

ESOP-2011-GawlitzaM

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

CADE-2011-BlanchetteBP

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

CADE-2011-DeharbeFMP #problem #symmetry

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

CADE-2011-HaarslevSV #automation #reasoning

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

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

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

CAV-2011-Lahiri #analysis #composition

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

TAP-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.

IFM-2010-FranzleTE #hybrid #probability

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 #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 #type system

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

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

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

ICSE-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.

ASPLOS-2010-EyermanE #modelling #probability #scheduling

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

DATE-2010-CimattiFGKR #abstraction #integration

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

DATE-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.

ICST-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.

SAT-2010-BofillSV #constraints #problem

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

SAS-2009-Qadeer #algorithm #using #verification

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

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

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

SAC-2009-LeinoM #first-order #reasoning

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

ASPLOS-2009-EyermanE #thread

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

TACAS-2009-BrummayerB #array #named #performance

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

CAV-2009-JhaLS #named #performance

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

CAV-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.

CAV-2009-SrivastavaGF #named #verification

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

CAV-2009-WintersteigerHM #approach #concurrent

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

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

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

POPL-2008-LahiriQ #precise #using #verification

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

DATE-2008-GanaiG #source code

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

HPCA-2008-RamirezPSV #performance #thread

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

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

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

TACAS-2008-Moskal #proving

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

TACAS-2008-MouraB #named #performance

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

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

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

CAV-2008-BofillNORR

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

CAV-2008-BruttomessoCFGS

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

IJCAR-2008-GhilardiNRZ #model checking #towards

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

HPCA-2007-EyermanE #parallel #policy

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

CADE-2007-MouraB #performance

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

CAV-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.

SAC-2006-Lo #protocol

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

HPCA-2006-SharkeyP #performance

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

TACAS-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.

CAV-2006-LahiriNO #abstraction #performance

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

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

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

SAT-2006-YuM #constraints #learning #linear

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

HPCA-2005-HasanJVB

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

HPCA-2005-LiBHS #architecture #energy #performance

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

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

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

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

ASPLOS-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.

HPCA-2003-El-MoursyA #performance #policy

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

HPCA-2003-RedstoneEL #named #thread

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

PDP-2002-GoncalvesN #performance #process #scheduling

Improving SMT Performance Scheduling Processes (RG, POAN), pp. 327–334.

PDP-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.

HPCA-2000-BurnsG #layout #question

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