Antti Hyvärinen: Publications by year
Last modified August 19, 2021.
To appear
- Theory-Specific Proof Steps Witnessing Correctness of SMT Executions
Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E. J. Hyvärinen, and Natasha Sharygina
To appear in the 58th Design Automation Conference (DAC 2021)
[pdf]
- Lookahead in Partitioning SMT
Antti E. J. Hyvärinen, Matteo Marescotti, and Natasha Sharygina
To appear in Formal Methods in Computer-Aided Design (FMCAD 2021)
[pdf]
2021
-
Using linear algebra in decomposition of Farkas interpolants
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, and Natasha Sharygina
International Journal on Software Tools for Technology Transfer (2021)
[pdf]
2020
-
Decomposing Farkas Interpolants
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, and Natasha Sharygina
TACAS 2019: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
[pdf]
-
Incremental Verification by SMT-Based Summary Repair
Sepideh Asadi, Martin Blicha, Antti Hyvärinen, Natasha Sharygina, and Grigory Fedyukovich
2020 Formal Methods in Computer Aided Design, FMCAD 2020
[pdf]
-
Accurate Smart Contract Verification Through Direct Modelling
Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, and Natasha Sharygina
Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020
[pdf]
-
Farkas-Based Tree Interpolation
Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, and Natasha Sharygina
Static Analysis - 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020, Proceedings
[pdf]
-
A Cooperative Parallelization Approach for Property-Directed k-Induction
Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, and Natasha Sharygina
Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings.
[pdf]
2019
-
Decomposing Farkas Interpolants
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, and Natasha Sharygina
TACAS 2019: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
[pdf]
-
Lattice-based SMT for Program Verification
Karine Even-Mendoza, Antti E. J. Hyvärinen, and Natasha Sharygina
MEMOCODE 2019
[pdf]
-
Exploiting Partial Variable Assignment in Interpolation-Based Model Checking
Pavel Jancik, Jan Kofron, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina
Formal Methods Syst. Des. 55(1): 33-71 (2019)
[pdf]
2018
-
Function Summarization Modulo Theories
Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Karine Even-Mendoza, Natasha Sharygina, and Hana Chockler
LPAR-22: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
[pdf]
-
SMTS: Distributed, Visualized Constraint Solving
Matteo Marescotti, Antti E. J. Hyvärinen, and Natasha Sharygina
LPAR-22: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
[pdf]
-
Lookahead-Based SMT Solving
Antti E. J. Hyvärinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, and Natasha Sharygina
LPAR-22: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
[pdf]
-
Parallel Satisfiability Modulo Theories
Antti E. J. Hyvärinen, Christoph M. Wintersteiger
Handbook of Parallel Constraint Reasoning
Youssef Hamadi and Lakhdar Sais
pages 141-178
Springer, 2018
[pdf]
-
Computing Exact Worst-Case Gas Consumption for Smart Contracts
Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi, and Natasha Sharygina
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2018)
[pdf]
-
Lattice-Based Refinement in Bounded Model Checking
Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, and Natasha Sharygina
10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018)
[pdf]
2017
-
HiFrog: SMT-based Function Summarization for Software Verification
Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina
Tools and Algorithms for the Construction and Analysis of Systems
- 23rd International Conference (TACAS 2017)
Axel Legay and Tiziana Margaria
pages 207-213
Springer, 2017
[pdf]
-
Theory Refinement for Program Verification
Antti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina
Theory and Applications of Satisfiability Testing (SAT 2017)
Serge Gaspers and Toby Walsh
pages 347 - 363
Springer, 2017
[pdf]
-
LRA Interpolants from No Man's Land
Leonardo Alt, Antti E. J. Hyvärinen, and Natasha Sharygina
Hardware and Software: Verification and Testing - 13th International
Haifa Verification Conference (HVC 2017)
Ofer Strichman and Rachel Tzoref-Brill
pages 195-210
Springer, 2017
[pdf]
-
Designing Parallel PDR
Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, and Natasha Sharygina
Formal Methods in Computer Aided Design (FMCAD 2017)
Daryl Stewart and Georg Weissenbacher
pages 156 - 163
IEEE, 2017
[pdf]
-
Duality-based interpolation for quantifier-free equalities and uninterpreted functions
Leonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, and Natasha Sharygina
Formal Methods in Computer Aided Design (FMCAD 2017)
Daryl Stewart and Georg Weissenbacher
pages 39--46
IEEE, 2017
[pdf]
2016
-
Clause Sharing and Partitioning for Cloud-Based SMT Solving
Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
Automated Technology for Verification and Analysis - 14th International
Symposium, (ATVA 2016)
Cyrille Artho, Axel Legay, and Doron Peled
pages 428-443
Springer, 2016
[pdf]
-
PVAIR: Partial Variable Assignment InterpolatoR
Pavel Jancík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofron, and Natasha Sharygina
Fundamental Approaches to Software Engineering - 19th International
Conference (FASE 2016)
Perdita Stevens and Andrzej Wasowski
pages 419-434
Springer, 2016
[pdf]
-
OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
Antti E. J. Hyvarinen, Matteo Marescotti, Leonardo Alt, and Natasha Sharygina
The 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)
Nadia Creignou and Daniel Le Berre,
pages 547-553
Springer, 2016
[pdf]
2015
-
Flexible Interpolation for Efficient Model Checking
Antti E. J. Hyvärinen, Leonardo Alt, and Natasha Sharygina
Mathematical and Engineering Methods in Computer Science - 10th International
Doctoral Workshop, MEMICS 2015, Telc, Czech Republic, October
23-25, 2015, Revised Selected Papers,
Jan Kofron and Tomas Vojnar,
pages 11-22
Springer, 2016
[pdf]
-
Search-Space Partitioning for Parallel SMT Solvers
Antti E. J. Hyvärinen, Matteo Marescotti, and Natasha Sharygina
The 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015),
Marijn Heule and Sean Weaver,
pages 369-386
[pdf]
-
A Proof-Sensitive Approach for Small Propositional Interpolants
Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina
7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2015),
Arie Gurfinkel, and Sanjit A. Seshia,
pages 1-18.
Springer 2015
[pdf]
-
The PeRIPLO Propositional Interpolator
Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina
In the 3rd Interpolation Workshop (collocated with CAV 2015). Abstract.
-
Optimizing Function Summaries Through Interpolation
Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina
In Validation of Evolving Software (book chapter),
Hana Chockler, Daniel Kroening, Leonardo Mariani, and Natasha Sharygina,
pages 73-82.
Springer 2015.
-
Regression Checking of Changes in C Software
Fabrizio Pastore, Leonardo Mariani, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt, and Ali Muhammad
In Validation of Evolving Software (book chapter),
Hana Chockler, Daniel Kroening, Leonardo Mariani, and Natasha Sharygina,
pages 185-207.
Springer 2015.
-
Symbolic Detection of Assertion Dependencies for Bounded Model Checking
Grigory Fedyukovich, Andrea Callia D'Iddio, Antti E. J. Hyvärinen, and Natasha Sharygina
In proceedings of the Fundamental Approaches to Software Engineering (FASE 2015),
Alexander Egyed and Ina Schaefer,
pages 186-201.
Springer 2015.
[pdf]
2014
-
Verification-Aided Regression Testing
Fabrizio Pastore, Leonardo Mariani, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehested, and Ali Muhammad
In proceedings of the International Symposium on Software Testing and Analysis (ISSTA 2014),
Corina S. Pasareanu and Darko Marinov,
pages 37-48.
ACM 2014.
[pdf]
2013
-
PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification
Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Hyvärinen, and Natasha Sharygina
In proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013),
Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov,
pages 683--693.
Springer, 2013.
[pdf]
-
Interpolation-based Model Checking for Efficient Incremental Analysis of
Software
Grigory Fedyukovich, Antti E. J. Hyvärinen and Natasha Sharygina
In proceedings of the 16th IEEE International Symposium on Design and
Diagnostics of Electronic Circuits & Systems (DDECS 2013),
Lukas Sekanina, Görschwin Fey, Jaan Raik, Snorre Aunet, and
Richard Ruzicka,
pages 8-9.
IEEE Computer Society, 2013.
[pdf]
-
PINCETTE - Validating Changes and Upgrades in Networked Software
Hana Chockler, Giovanni Denaro, Meijia Ling, Grigory Fedyukovich, Antti Eero
Johannes Hyvärinen, Leonardo Mariani, Ali Muhammad, Manuel Oriol, Ajitha
Rajan, Ondrej Sery, Natasha Sharygina, and Michael Tautschnig
In proceedings of the
17th European Conference on Software Maintenance and Reengineering (CSMR 2013),
Anthony Cleve, Filippo Ricca, and Maura Cerioli
pages 461 - 464.
IEEE Computer Society, 2013
2012
-
Designing Scalable Parallel SAT Solvers
Antti E. J. Hyvärinen and Norbert Manthey
In Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012),
A. Cimatti and R. Sebastiani, editors,
volume 7317 of Lecture Notes in Computer Science,
pages 214 -- 227.
Springer, 2012
[pdf]
-
Approaches for Multi-Core Propagation in Clause Learning Satisfiability Solvers
Antti E. J. Hyvärinen and Christoph M. Wintersteiger
no. MSR-TR-2012-47
Mircrosoft Research, 1 May 2012
[pdf]
2011
-
Grid Based Propositional Satisfiability Solving
Antti E. J. Hyvärinen.
Doctoral Dissertation,
Aalto University publication series
Doctoral Dissertations 118/2011
Aalto Print
Helsinki 2011
Finland
[pdf]
-
Grid-Based SAT Solving with Iterative Partitioning and Clause
Learning
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
17th International Conference on Principles and Practice of
Constraint Programming (CP 2011),
J. Lee, editor,
volume 6876 of Lecture Notes in Computer Science,
pages 385 -- 399.
Springer, 2011
[pdf]
-
Partitioning Search Spaces of a Randomized Search
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
Fundamenta Informaticae, 107(2011)
pages 289-311.
[pdf]
2010
-
Partitioning SAT Instances for Distributed Solving
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
17th International Conference on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR2010),
C. Fermüller, A. Voronkov, editors,
volume 6397 of Lecture Notes in Computer Science,
pages 372-386.
Springer, 2010
-
Partitioning SAT Instances for Distributed Solving
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
3rd International Workshop on Logic and Search (LaSh2010)
[pdf]
2009
-
Partitioning Search Spaces of a Randomized Search
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
11th Conference of the Italian Association for Artificial
Intelligence (AI*IA 2009),
Roberto Serra, Rita Cucchiara, editors,
volume 5883 of Lecture Notes in Artificial Intelligence,
pages 243-252.
Springer, 2009.
[pdf]
-
Partitioning Search Spaces of a Randomized Search (extended version)
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
The original publication will appear in Proceedings of the
11th Conference of the Italian Association for Artificial
Intelligence (AI*IA 2009), and will be available at www.springerlink.com.
[pdf]
-
Incorporating Clause Learning in Grid-Based Randomized SAT Solving
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
Journal on Satisfiability, Boolean Modeling and Computation, 6(2009)
pages 223-244.
[pdf]
-
Approaches to Grid-Based SAT Solving
Antti E. J. Hyvärinen. Research Report TKK-ICS-R16 ,
Helsinki University of Technology,
Department of Information and Computer Science
Espoo, Finland,
May 2009.
Note: A reprint of the Licentiate's Thesis
[ps]
[pdf]
[abstract/bibtex]
-
Approaches to Grid-Based SAT Solving
Antti E. J. Hyvärinen. Licentiate's Thesis,
Helsinki University of Technology,
Laboratory for Theoretical Computer Science,
Espoo, Finland,
March 2009.
[pdf]
2008
-
Incorporating Learning in Grid-Based Randomized SAT Solving
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
13th International Conference on Artificial Intelligence: Methodology,
Systems, Applications (AIMSA 2008),
Daniel Dochev, Marco Pistore, Paolo Traverso, editors,
volume 5253 of Lecture Notes in Artificial Intelligence,
pages 247-261.
Springer, 2008.
[ps]
[pdf]
[abstract/bibtex]
-
Strategies for solving SAT in Grids by randomized search
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
9th International Conference on
Artificial Intelligence and Symbolic Computation (AISC
2008),
Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu
Suzuki, and Freeke Wiedijk, editors,
volume 5144 of Lecture Notes in Artificial Intelligence,
pages 125-140.
Springer, 2008.
[ps]
[pdf]
[abstract/bibtex]
-
Using the Grid for Enhancing the Performance of a
Medical Image Search Engine
Mikko Juhani Pitkanen, Xin Zhou, Antti E. J. Hyvärinen, and Henning
Müller
In Proceedings of the
21st IEEE International Symposium on Computer-Based Medical Systems
(IEEE CBMS 2008),
Seppo Puuronen, Mykola Pechenizkiy, Alexey Tsymbal, and Dah-Jye Lee,
editors,
pages 367-372.
IEEE Computer Society, 2008
[ps]
[pdf]
[abstract/bibtex]
2006
-
A Distribution Method for Solving SAT in Grids
Antti E. J. Hyvärinen,
Tommi Junttila, and Ilkka Niemelä
In Proceedings of the
9th International Conference on Theory and Applications of
Satisfiability Testing (SAT 2006),
Armin Biere and Carla P. Gomes, editors,
volume 4121 of
Lecture Notes in Computer Science,
pages 430-435.
Springer, 2006.
[ps]
[pdf]
[abstract/bibtex]
[extended
version ps]
[extended
version pdf]
-
Lauselogiikan toteutuvuusongelman ratkaiseminen laskennallisessa
gridissä
Antti E. J. Hyvärinen,
In Lea Kutvonen, and Päivi Kuuppelomäki,
editors, Tietojenkäsittelytieteen päivät 2006 ,
volume B-2006-3 of Tietojenkäsittelytieteen laitoksen julkaisjua
sarja B
pages 37-43.
Tietojenkäsittelytieteen laitos, 2006.
[ps]
[pdf]
[abstract/bibtex]
-
SATU: A system for distributed propositional
satisfiability checking in computational grids
Antti E. J. Hyvärinen. Research Report A100 ,
Helsinki University of Technology,
Laboratory for Theoretical Computer Science,
Espoo, Finland,
[pdf]
[abstract/bibtex]
2005
-
SATU: A system for distributed propositional
satisfiability checking in computational grids
Antti E. J. Hyvärinen. Master's Thesis,
Helsinki University of Technology,
Laboratory for Theoretical Computer Science,
Espoo, Finland,
February 2006.