Search results for "SMT"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
35	Sava Krstic, Albert Oliveras	Preface.	SMT@CAV	2007	DBLP DOI BibTeX RDF
35	Michal Moskal, Jakub Lopuszanski, Joseph R. Kiniry	E-matching for Fun and Profit.	SMT@CAV	2007	DBLP DOI BibTeX RDF
35	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Model-based Theory Combination.	SMT@CAV	2007	DBLP DOI BibTeX RDF
35	Mirron Rozanov, Ofer Strichman	Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic.	SMT@CAV	2007	DBLP DOI BibTeX RDF
35	Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer	CC(X): Semantic Combination of Congruence Closure with Solvable Theories.	SMT@CAV	2007	DBLP DOI BibTeX RDF
32	Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia	Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic.	CAV	2009	DBLP DOI BibTeX RDF
32	Armin Biere	SAT, SMT and Applications.	LPNMR	2009	DBLP DOI BibTeX RDF
32	Robert Brummayer, Armin Biere	Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.	TACAS	2009	DBLP DOI BibTeX RDF
32	Alessandro Armando	Building SMT-Based Software Model Checkers: An Experience Report.	FroCoS	2009	DBLP DOI BibTeX RDF
32	Jonathan A. Winter, David H. Albonesi	Addressing thermal nonuniformity in SMT workloads.	ACM Trans. Archit. Code Optim.	2008	DBLP DOI BibTeX RDF	adaptive microarchitectures, dynamic voltage scaling, Simultaneous multithreading, dynamic thermal management, clustered microarchitectures
32	Joseph J. Sharkey, Jason Loew, Dmitry V. Ponomarev	Reducing register pressure in SMT processors through L2-miss-driven early register release.	ACM Trans. Archit. Code Optim.	2008	DBLP DOI BibTeX RDF	register file, Simultaneous multithreading
32	Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio	The Barcelogic SMT Solver.	CAV	2008	DBLP DOI BibTeX RDF
32	Hongzhou Chen, Lingdi Ping, Xuezeng Pan, Kuijun Lu, Xiaoping Chen	A Dissipative Resource Distribution policy for SMT processors.	IPDPS	2008	DBLP DOI BibTeX RDF
32	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Z3: An Efficient SMT Solver.	TACAS	2008	DBLP DOI BibTeX RDF
32	Geoffrey M. Brown, Lee Pike	Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols.	MEMOCODE	2007	DBLP DOI BibTeX RDF
32	Zhibin Zhang, Li Guo 0001, Binxing Fang, Xiaojun Chen 0004	Parallelizing Protocol Processing on SMT Processor Efficiently: A FSM Decomposition Approach.	IPCCC	2007	DBLP DOI BibTeX RDF
32	David Walter, Scott Little, Chris J. Myers	Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver.	ATVA	2007	DBLP DOI BibTeX RDF
32	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Efficient E-Matching for SMT Solvers.	CADE	2007	DBLP DOI BibTeX RDF
32	Joseph J. Sharkey, Dmitry V. Ponomarev	An L2-miss-driven early register deallocation for SMT processors.	ICS	2007	DBLP DOI BibTeX RDF	register files, simultaneous multithreading
32	Qingying Deng, Minxuan Zhang, Jiang Jiang	A Parallel Infrastructure on Dynamic EPIC SMT and Its Speculation Optimization.	ISPA	2007	DBLP DOI BibTeX RDF
32	Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar	Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.	FMCAD	2007	DBLP DOI BibTeX RDF
32	Sonia López, Steve Dropsho, David H. Albonesi, Oscar Garnica, Juan Lanchares	Dynamic Capacity-Speed Tradeoffs in SMT Processor Caches.	HiPEAC	2007	DBLP DOI BibTeX RDF
32	Kenneth Roe	The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover.	CAV	2006	DBLP DOI BibTeX RDF
32	Joseph J. Sharkey, Dmitry V. Ponomarev	Efficient instruction schedulers for SMT processors.	HPCA	2006	DBLP DOI BibTeX RDF
32	Hossein M. Sheini, Karem A. Sakallah	SMT(CLU): a step toward scalability in system verification.	ICCAD	2006	DBLP DOI BibTeX RDF
32	Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.	TACAS	2006	DBLP DOI BibTeX RDF
32	Joseph J. Sharkey, Dmitry Ponomarev 0001	Balancing ILP and TLP in SMT Architectures through Out-of-Order Instruction Dispatch.	ICPP	2006	DBLP DOI BibTeX RDF
32	Caixia Sun, Hong-Wei Tang, Minxuan Zhang	Controlling Performance of a Time-Criticial Thread in SMT Processors by Instruction Fetch Policy.	PDCAT	2006	DBLP DOI BibTeX RDF
32	Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump	SMT-COMP: Satisfiability Modulo Theories Competition.	CAV	2005	DBLP DOI BibTeX RDF
32	Hua Yang, Gang Cui, Xiao-Zong Yang	2L-MuRR: A Compact Register Renaming Scheme for SMT Processors.	ISPA	2005	DBLP DOI BibTeX RDF
32	Muhamed F. Mudawar	Scalable cache memory design for large-scale SMT architectures.	WMPI	2004	DBLP DOI BibTeX RDF	scalable multiported cache memory, simultaneous multithreaded architectures
32	Francisco J. Cazorla, Peter M. W. Knijnenburg, Rizos Sakellariou, Enrique Fernández, Alex Ramírez, Mateo Valero	Implicit vs. Explicit Resource Allocation in SMT Processors.	DSD	2004	DBLP DOI BibTeX RDF
32	Francisco J. Cazorla, Peter M. W. Knijnenburg, Rizos Sakellariou, Enrique Fernández, Alex Ramírez, Mateo Valero	Feasibility of QoS for SMT.	Euro-Par	2004	DBLP DOI BibTeX RDF
32	Joshua L. Kihm, Daniel A. Connors	Implementation of Fine-Grained Cache Monitoring for Improved SMT Scheduling.	ICCD	2004	DBLP DOI BibTeX RDF
32	Joshua Redstone, Susan J. Eggers, Henry M. Levy	Mini-Threads: Increasing TLP on Small-Scale SMT Processors.	HPCA	2003	DBLP DOI BibTeX RDF
32	Leandro G. Barajas, Ashish Kansal, Abhinav Saxena, Magnus Egerstedt, Alex Goldstein, Edward W. Kamen	Modeling and Control of SMT Manufacturing Lines Using Hybrid Dynamic Systems.	HSCC	2003	DBLP DOI BibTeX RDF
32	Chulho Shin, Seong-Won Lee, Jean-Luc Gaudiot	Dynamic Scheduling Issues in SMT Architectures.	IPDPS	2003	DBLP DOI BibTeX RDF
32	Jörg Mische, Sascha Uhrig, Florian Kluge, Theo Ungerer	Using SMT to Hide Context Switch Times of Large Real-Time Tasksets.	RTCSA	2010	DBLP DOI BibTeX RDF	hardware scheduler, in-order multithreading, hard real-time, SMT, context switch
32	Yongliang Ma, Tiejun Zhao	Improving Chinese to English SMT with Multiple CWS Results.	IALP	2009	DBLP DOI BibTeX RDF	feature blending, feature interpolation, SMT, Chinese word segmentation
29	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Interpolant Generation for UTVPI.	CADE	2009	DBLP DOI BibTeX RDF
29	Hyondeuk Kim, Fabio Somenzi, HoonSang Jin	Efficient Term-ITE Conversion for Satisfiability Modulo Theories.	SAT	2009	DBLP DOI BibTeX RDF
29	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Satisfiability Modulo Theories: An Appetizer.	SBMF	2009	DBLP DOI BibTeX RDF
29	Malay K. Ganai, Franjo Ivancic	Efficient decision procedure for non-linear arithmetic constraints using CORDIC.	FMCAD	2009	DBLP DOI BibTeX RDF
29	Kenzo Van Craeynest, Stijn Eyerman, Lieven Eeckhout	MLP-Aware Runahead Threads in a Simultaneous Multithreading Processor.	HiPEAC	2009	DBLP DOI BibTeX RDF
29	Evangelia Athanasaki, Nikos Anastopoulos, Kornilios Kourtis, Nectarios Koziris	Exploring the performance limits of simultaneous multithreading for memory intensive applications.	J. Supercomput.	2008	DBLP DOI BibTeX RDF	Speculative precomputation, Performance analysis, Instruction-level parallelism, Thread-level parallelism, Simultaneous multithreading, Software prefetching
29	Peter Rounce, Alberto Ferreira de Souza	Dynamic Instruction Scheduling in a Trace-based Multi-threaded Architecture.	Int. J. Parallel Program.	2008	DBLP DOI BibTeX RDF	Simultaneous multi-threading, Wide issue architectures, VLIW, Dynamic instruction scheduling
29	Adam Lopez	Statistical machine translation.	ACM Comput. Surv.	2008	DBLP DOI BibTeX RDF	Natural language processing, machine translation
29	Tommi A. Junttila, Jori Dubrovin	Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking.	LPAR	2008	DBLP DOI BibTeX RDF
29	Kshitiz Malik, Mayank Agarwal, Vikram Dhar, Matthew I. Frank	PaCo: Probability-based path confidence prediction.	HPCA	2008	DBLP DOI BibTeX RDF
29	Martin Fränzle, Holger Hermanns, Tino Teige	Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems.	HSCC	2008	DBLP DOI BibTeX RDF
29	Hong-Nhung Nguyen Thi, Dien Dinh	A Syntactic-based Word Re-ordering for English-Vietnamese Statistical Machine Translation System.	PRICAI	2008	DBLP DOI BibTeX RDF	word re-ordering, syntactic-based word re-ordering rule, Statistical machine translation, parse tree
29	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Engineering DPLL(T) + Saturation.	IJCAR	2008	DBLP DOI BibTeX RDF
29	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	Efficient Interpolant Generation in Satisfiability Modulo Theories.	TACAS	2008	DBLP DOI BibTeX RDF
29	Germán Sanchis-Trilles, Maria-Teresa González, Francisco Casacuberta, Enrique Vidal 0001, Jorge Civera	Introducing Additional Input Information into Interactive Machine Translation Systems.	MLMI	2008	DBLP DOI BibTeX RDF	Interactive MT, Computer Assisted Translation
29	Joseph J. Sharkey, Dmitry V. Ponomarev	Exploiting Operand Availability for Efficient Simultaneous Multithreading.	IEEE Trans. Computers	2007	DBLP DOI BibTeX RDF	simultaneous multithreading, Issue queue
29	Nitzan Peleg, Bilha Mendelson	Detecting Change in Program Behavior for Adaptive Optimization.	PACT	2007	DBLP DOI BibTeX RDF
29	Manoj Gupta 0001, Fermín Sánchez, Josep Llosa	Merge Logic for Clustered Multithreaded VLIW Processors.	DSD	2007	DBLP DOI BibTeX RDF
29	Lin Xu, Xiaoguang Cao, Bufeng Zhang, Mu Li 0001	Comparing and Integrating Alignment Template and Standard Phrase-Based Statistical Machine Translation.	CICLing	2007	DBLP DOI BibTeX RDF
29	Kyueun Yi, Jean-Luc Gaudiot	Architectural Support for Network Applications on Simultaneous MultiThreading Processors.	IPDPS	2007	DBLP DOI BibTeX RDF
29	Xing Fang, Dong Wang, Shuming Chen	Exploiting Thread-Level Parallelism of Irregular LDPC Decoder with Simultaneous Multi-threading Technique.	APPT	2007	DBLP DOI BibTeX RDF
29	Maria Paola Bonacina, Mnacho Echenim	T-Decision by Decomposition.	CADE	2007	DBLP DOI BibTeX RDF
29	Manoj Gupta 0001, Fermín Sánchez, Josep Llosa	Cluster-level simultaneous multithreading for VLIW processors.	ICCD	2007	DBLP DOI BibTeX RDF
29	Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio	Challenges in Satisfiability Modulo Theories.	RTA	2007	DBLP DOI BibTeX RDF
29	Seong-Won Lee, Jean-Luc Gaudiot	Throttling-Based Resource Management in High Performance Multithreaded Architectures.	IEEE Trans. Computers	2006	DBLP DOI BibTeX RDF	Resource management, power management, multithreading, resource utilization, throttling
29	Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T).	J. ACM	2006	DBLP DOI BibTeX RDF	SAT solvers, Satisfiability Modulo Theories
29	Panagiotis Papadimitratos, Zygmunt J. Haas	Secure data communication in mobile ad hoc networks.	IEEE J. Sel. Areas Commun.	2006	DBLP DOI BibTeX RDF
29	Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Splitting on Demand in SAT Modulo Theories.	LPAR	2006	DBLP DOI BibTeX RDF
29	Daniele Paolo Scarpazza, Praveen Raghavan, David Novo, Francky Catthoor, Diederik Verkest	Software Simultaneous Multi-Threading, a Technique to Exploit Task-Level Parallelism to Improve Instruction- and Data-Level Parallelism.	PATMOS	2006	DBLP DOI BibTeX RDF
29	Thai Phuong Nguyen, Akira Shimazu	A Syntactic Transformation Model for Statistical Machine Translation.	ICCPOL	2006	DBLP DOI BibTeX RDF
29	In-Pyo Hong, Yong-Joo Lee, Yong-Surk Lee	Next Generation Embedded Processor Architecture for Personal Information Devices.	EUC	2006	DBLP DOI BibTeX RDF
29	Wessam Hassanein, Moustafa A. Hammad, Layali K. Rashid	Characterizing the Performance of Data Management Systems on Hyper-Threaded Architectures.	SBAC-PAD	2006	DBLP DOI BibTeX RDF
29	Bin Wang, Chaojian Shi	A Novel Split-and-Merge Technique for Error-Bounded Polygonal Approximation.	ICONIP (2)	2006	DBLP DOI BibTeX RDF
29	Michael Carl	A system-theoretical view of EBMT.	Mach. Transl.	2005	DBLP DOI BibTeX RDF	Statistical EBMT, Statistical machine translation, System theory, Example-based machine translation, Emergent behaviour
29	Robert Nieuwenhuis, Albert Oliveras	Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools.	LPAR	2005	DBLP DOI BibTeX RDF
29	Yun Zhang, Michael Voss	Runtime Empirical Selection of Loop Schedulers on Hyperthreaded SMPs.	IPDPS	2005	DBLP DOI BibTeX RDF
29	Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz 0001, Roberto Sebastiani	The MathSAT 3 System.	CADE	2005	DBLP DOI BibTeX RDF
29	Ali El-Haj-Mahmoud, Ahmed S. Al-Zawawi, Aravindh Anantaraman, Eric Rotenberg	Virtual multiprocessor: an analyzable, high-performance architecture for real-time computing.	CASES	2005	DBLP DOI BibTeX RDF	worst-case execution time, schedulability analysis, superscalar processor, simultaneous multithreading, hard real-time, resource partitioning
29	Hai Zhou 0001	Efficient Steiner tree construction based on spanning graphs.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2004	DBLP DOI BibTeX RDF
29	Liem Tran, Nicholas Nelson 0001, Fung Ngai, Steve Dropsho, Michael C. Huang 0001	Dynamically reducing pressure on the physical register file through simple register sharing.	ISPASS	2004	DBLP DOI BibTeX RDF
29	Christian Tenllado, Carlos García 0001, Manuel Prieto 0001, Luis Piñuel, Francisco Tirado	Exploiting Multilevel Parallelism Within Modern Microprocessors: DWT as a Case Study.	VECPAR	2004	DBLP DOI BibTeX RDF
29	Alon Lavie, Stephan Vogel, Lori S. Levin, Erik Peterson, Katharina Probst, Ariadna Font Llitjós, Rachel Reynolds, Jaime G. Carbonell, Richard Cohen	Experiments with a Hindi-to-English transfer-based MT system under a miserly data scenario.	ACM Trans. Asian Lang. Inf. Process.	2003	DBLP DOI BibTeX RDF	limited data resources, multiengine machine translation, transfer rules, machine learning, Evaluation, Hindi, example-based machine translation, statistical translation
29	Daniel Ortiz, Ismael García-Varea, Francisco Casacuberta	An Empirical Comparison of Stack-Based Decoding Algorithms for Statistical Machine Translation.	IbPRIA	2003	DBLP DOI BibTeX RDF
29	Philippe Langlais	Opening Statistical Translation Engines to Terminological Resources.	NLDB	2002	DBLP DOI BibTeX RDF
29	Philippe Langlais, Michel Simard	Merging Example-Based and Statistical Machine Translation: An Experiment.	AMTA	2002	DBLP DOI BibTeX RDF
29	Y. Y. Li, Kwong-Sak Leung, C. K. Wong	Steiner Trees in General Nonuniform Orientations.	Computing	2001	DBLP DOI BibTeX RDF
29	Allan Snavely, Dean M. Tullsen	Symbiotic Jobscheduling for a Simultaneous Multithreading Processor.	ASPLOS	2000	DBLP DOI BibTeX RDF
29	Perfecto Mariño, Miguel Angel Domínguez	Integration of Image Processing and Automated Testing in a Manufacturing Client-Server Network.	EUROMICRO	1998	DBLP DOI BibTeX RDF
29	Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari 0001	Oracle-guided component-based program synthesis.	ICSE (1)	2010	DBLP DOI BibTeX RDF	oracle-based learning, SAT, program synthesis, SMT
29	Malay K. Ganai, Aarti Gupta	Tunneling and slicing: towards scalable BMC.	DAC	2008	DBLP DOI BibTeX RDF	CFG, partitioning, slice, SMT, tunnel, EFSM, CSR, BMC
28	William R. Harris, Sriram Sankaranarayanan 0001, Franjo Ivancic, Aarti Gupta	Program analysis via satisfiability modulo path programs.	POPL	2010	DBLP DOI BibTeX RDF	program analysis, abstract interpretation, symbolic execution, path sensitivity, smt solvers, satisfiability solvers
28	Dongyoon Lee, Mahmoud Said, Satish Narayanasamy, Zijiang Yang 0006, Cristiano Pereira	Offline symbolic analysis for multi-processor execution replay.	MICRO	2009	DBLP DOI BibTeX RDF	multi-processor replay, shared-memory dependencies, SMT solver
28	Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer	Unifying type checking and property checking for low-level code.	POPL	2009	DBLP DOI BibTeX RDF	assertion checking, low-level code, decision procedure, type checking, smt solver, property checking
28	Levent Erkök, John Matthews	Pragmatic equivalence and safety checking in Cryptol.	PLPV	2009	DBLP DOI BibTeX RDF	sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking
28	Saurabh Srivastava 0001, Sumit Gulwani	Program verification using templates over predicate abstraction.	PLDI	2009	DBLP DOI BibTeX RDF	constraint-based fixed-point, iterative fixed-point, quantified invariants, template invariants, predicate abstraction, weakest preconditions, smt solvers
28	Xiuzhen Cheng 0001, Ding-Zhu Du, Lusheng Wang 0001, Baogang Xu	Relay sensor placement in wireless sensor networks.	Wirel. Networks	2008	DBLP DOI BibTeX RDF	Relay sensor, SMT-MSP, Wireless sensor networks, Topology control, Steiner point
28	Vimal K. Reddy, Eric Rotenberg, Sailashri Parthasarathy	Understanding prediction-based partial redundant threading for low-overhead, high- coverage fault tolerance.	ASPLOS	2006	DBLP DOI BibTeX RDF	redundant multithreading, simultaneous multithreading (SMT), slipstream processor, chip multiprocessor (CMP), branch prediction, transient faults, value prediction, time redundancy
28	Guansong Zhang, Priya Unnikrishnan, James Ren	Experiments with Auto-Parallelizing SPEC2000FP Benchmarks.	LCPC	2004	DBLP DOI BibTeX RDF	SMT machine, parallel do, OpenMP, parallelizing compiler, automatic parallelization
25	Weijie Wang, Yan Wang 0081, Guokun Xu, Qiujian Lv, Zuxin Chen, Siyuan Li	VN-SMT: An SMT-based Construction Method on Virtual Network to Defend Insider Reconnaissance.	WCNC	2023	DBLP DOI BibTeX RDF
25	Hans-Jörg Schurr	Stronger SMT Solvers for Proof Assistants: Proofs, Quantifier Simplification, Strategy Schedules. (Consolidation des solveurs SMT pour les assistants de preuve: preuves, simplification des quantificateurs, planification de stratégies).		2022	RDF
25	Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett	Smt-Switch: A Solver-Agnostic C++ API for SMT Solving.	SAT	2021	DBLP DOI BibTeX RDF