Public Area

Table of Contents

 

Publications

2008

Marques-Silva, J., Lynce, I. and Manquinho, V.
"Symmetry Breaking for Maximum Satisfiability",
International Conference on Logic for Programming Artificial Intelligence and Reasoning,
22-27 November 2008, Doha, Qatar

Josep Argelich, Chu-Min Li, Felip Manyà, Jordi Planes,
"The First and Second Max-SAT Evaluations",
Journal on Satisfiability, Boolean Modeling and Computation 4, (2008), pp. 251-278

Liffiton, M., Mneimneh, M., Lynce, I., Andraus, Z., Marques-Silva, J. and Sakallah, K.,
"A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas",
Constraints: An International Journal, accepted 2008

N.Bombieri, F.Fummi, G.Pravadelli,
“Reuse and Optimization of Testbenches and Properties in a TLM to RTL Design Flow”,
ACM Transactions on Design Automation of Electronic Systems (TODAES),
July 2008, vol. 47, no. 13, pp. 1-22

N. Bombieri, F. Fummi, G. Pravadelli,
“RTL-TLM Equivalence Checking Based on Simulation”,
IEEE East-West Design & Test Symposium (EWDTS),
Lviv, Ukraine, October 9-13, 2008, pp. 214-218

V. Guarnieri, F. Fummi, C. Marconcini, G. Pravadelli,
“An Optimized CLP-based Technique for Generating Propagation Sequences”,
IEEE East-West Design & Test Symposium (EWDTS),
Lviv, Ukraine, October 9-13, 2008, pp. 25-28

Matos, P., Planes, J., Letombe, F. and Marques-Silva, J.
"An Algorithm Porfolio for MAX-SAT",
European Conference on Artificial Intelligence, July 2008, Patras, Greece

Marques-Silva, J. and Planes, J.
"Algorithms for Maximum Satisfiability using Unsatisfiable Cores",
Design, Automation and Test in Europe Conference and Exhibition,
March 2008,Munich, Germany

Letombe, F. and Marques-Silva, J.
"Improvements to Hybrid Incremental SAT Algorithms",
International Conference on Theory and Applications of Satisfiability Testing,
May 2008, Guangzhou, China

Matos, P. and Marques-Silva, J.
"Model Checking Event-B by Encoding into Alloy",
ABZ2008, September 2008, London, UK

Marques-Silva, J.
"Model Checking with Boolean Satisfiability",
Journal of Algorithms in Cognition, Informatics and Logic, vol. 63 (1-3), pp. 3-16

Heras, F., Manquinho, V. and Marques-Silva, J,
"On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization",
International FLAIRS Conference, May 2008, Florida, USA

Marques-Silva, J.
"Practical Applications of Boolean Satisfiability",
Workshop on Discrete Event Systems (WODES'08),
May 2008, Goteborg, Sweden

Marques-Silva, J. and Manquinho, V.
"Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms",
International Conference on Theory and Applications of Satisfiability Testing,
May 2008, Guangzhou, China

Maksim Jenihhin, Jaan Raik, Raimund Ubar, Anton Chepurov.
"On reusability of verification assertions for testing",
IEEE Baltic Electronic Conference, 2008

Karina Minakova, Uljana Reinsalu, Anton Chepurov, Jaan Raik, Maksim Jenihhin,
Raimund Ubar, Peeter Ellervee.
"High-Level Decision Diagram Manipulations for Code Coverage Analysis",
IEEE Baltic Electronic Conference, 2008

Maksim Jenihhin, Jaan Raik, Anton Chepurov, Raimund Ubar.
"Temporally Extended High-Level Decision Diagrams for PSL Assertions Simulation",
Proceedings of the 13th IEEE European Test Symposium, IEEE Computer Society,
Los Alamitos, USA, May 2008

Jaan Raik, Raimund Ubar, Maksim Jenihhin, Anton Chepurov,
"PSL Assertion Checking with Temporally Extended High-Level Decision Diagrams",
9th IEEE Latin American Test Workshop, 17-20 February, 2008, Puebla, Mexico

Jaan Raik, Maksim Jenihhin, Anton Chepurov, Uljana Reinsalu, Raimund Ubar,
"APRICOT: a Framework for Teaching Digital Systems Verification",
19th EAEEIE Annual Conference, June 29 - July 2, 2008, Tallinn, Estonia

Jaan Raik, Raimund Ubar, Taavi Viilukas, Maksim Jenihhin,
"Mixed Hierarchical-Functional Fault Models for Targeting Sequential Cores",
Elsevier Journal of Systems Architecture, Elsevier, 2008

Jaan Raik, Uljana Reinsalu, Raimund Ubar, Maksim Jenihhin, Peeter Ellervee,
"Fast Code Coverage Analysis using High-Level Decision Diagrams",
Proceedings of the 11th IEEE Workshop on Design and Diagnostics of
Electronic Systems (DDECS), IEEE Computer Society, April 2008

Soheil Samii, Sergiu Rafiliu, Petru Eles, Zebo Peng,
"A Simulation Methodology for Worst-Case Response Time Estimation
of Distributed Real-Time Systems",
Proceedings of Design, Automation, and Test in Europe (DATE 2008),
Munich, Germany, 10-14 March, 2008, pp. 556-561

N. Bombieri, F. Fummi, G. Pravadelli,
“A Mutation Model for the SystemC TLM 2.0 Communication Interfaces”,
Proceedings of ACM/IEEE Design, Automation and Test in Europe (DATE),
Munich, Germany, 10-14 March, 2008, pp. 396-401

L. Di Guglielmo, F. Fummi, G. Pravadelli,
“Vacuity Analysis by Fault Simulation”,
Proceedings of ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2008

N. Bombieri, N. Deganello, F. Fummi
“Integrating RTL IPs into TLM Designs Through Automatic Transactor Generation”,
Proceedings of ACM/IEEE Design, Automation and Test in Europe (DATE),
Munich, Germany, 10-14 March, 2008, pp. 15-20

Jaan Raik, Hideo Fujiwara, Raimund Ubar, Anna Krivenko,
" Untestable Fault Identification in Sequential Circuits Using Model-Checking",
The 17th Asian Test Symposium (ATS 2008), IEEE, November 24-27, 2008, Sapporo, Japan, pp. 667-672

Jaan Raik, Hideo Fujiwara, Anna Krivenko,
" RT-Level Identification of Potentially Testable Initialization Faults",
The Ninth IEEE Workshop on RTL and High Level Testing (WRTLT 2008), IEEE, November 27-28, 2008, Sapporo, Japan, pp. 667-672

Anton Chepurov, Giuseppe Di Guglielmo, Franco Fummi, Graziano Pravadelli, Jaan Raik, Raimund Ubar, Taavi Viilukas,
"Automatic Generation of EFSMs and HLDDs for Functional ATPG",
11th IEEE Biennial Baltic Electronics Conference, October 6-8, 2008, Laulasmaa, Estonia, pp. 143-146

Maksim Jenihhin, Jaan Raik, Anton Chepurov, Raimund Ubar,
" PSL Assertion-Checking Using Temporally Extended High-Level Decision Diagrams", Springer Journal of Electronic Testing: Theory and Applications, under review

D. Karlsson, P. Eles, and Z. Peng,
" Transactor-Based Formal Verification of Real-time Embedded Systems", Book Chapter in Embedded Systems Specification and Design Languages (E. Villar, editor), Springer, ISBN: 978-1-4020-8296-2, 2008, pp. 255-270

 

2007

N.Bombieri, F. Fummi,
“Automatic Transactor Generation in TLM by Exploiting EFSMs”,
Proceedings of Design & Verification Conference & Exhibition (DVCon),
San Jose, CA, USA, 21-23 February, 2007, pp. 151- 158

Maksim Jenihhin, Jaan Raik, Anton Chepurov, Raimund Ubar,
"Assertion Checking with PSL and High-Level Decision Diagrams",
Proceedings of the IEEE 8th Workshop on RTL and High Level Testing (WRTLT'07), October 12-13, 2007, Beijing, P.R.China

F. Fummi, I.G. Harris, C, Marconcini, G. Pravadelli,
“A CLP-based Functional ATPG for Extended FSMs”,
Proceedings of IEEE International Workshop on Microprocessor Test and Verification (MTV),
Austin, TX, USA, 5-6 December, 2007

Daniel Karlsson, Petru Eles, Zebo Peng,
"Formal Verification of Component-based ",
Journal of Design Automation for Embedded Systems,
March 2007, vol. 11, no. 1, pp. 49-90

Daniel Karlsson, Petru Eles, Zebo Peng,
"Transactor-based Formal Verification of Real-time Embedded Systems",
Proceedings of Forum on specification and Design Languages (FDL),
Barcelona, Spain, 18-20 September 2007

Marques-Silva, J.
"Interpolant Learning and Reuse in SAT-Based Model Checking" ,
Electronic Notes in Theoretical Computer Science, 2007, vol. 174 (3) pp. 31-43

Lynce, I. and Marques-Silva, J.
"Random Backtracking in Backtrack Search Algorithms for Satisfiability",
Discrete Applied Mathematics, 2007, vol. 155(12) pp. 1604-1612

Lynce, I. and Marques-Silva, J.
"Breaking Symmetries in SAT Matrix Models" ,
Proceedings of International Conference on Theory and Applications of Satisfiability Testing (SAT), Lisbon, Portugal, May 2007

Bombieri, N., Fummi, F., Pravadelli, G. and Marques-Silva, J.
"Towards Equivalence Checking Between TLM and RTL Models" ,
Proceedings of Fifth ACM-IEEE International Conference on Formal Methods
and Models for Codesign (MEMOCODE), Nice, France. May 2007

Marques-Silva, J. and Lynce, I.
"Towards Robust CNF Encodings of Cardinality Constraints",
Proceedings of International Conference on Principles and Practice of Constraint Programming (CP), Providence, RI, USA, July 2007

N. Bombieri, A. Fedeli, F. Fummi, G. Pravadelli,
"Hybrid Incremental Assertion-Based Verification for TLM Design Flows",
IEEE Design &Test of Computers, 2007

Andrea Fedeli, Franco Fummi, Graziano Pravadelli,
"Properties Incompleteness Evaluation by Functional Verification",
IEEE Transactions on Computers, 2007, vol. 56, n. 4

F. Fummi, G. Pravadelli,
"Too Few or Too Many Properties? Measure it by ATPG",
Journal of Electronic Testing: Theory and Applications, 2007

G. Di Guglielmo, F. Fummi, C. Marconcini, G. Pravadelli
"Improving High-Level and Gate-Level Testing with FATE: A Functional ATPG Traversing Unstabilized EFSMs"
IET Computers & Digital Techniques, 2007

G. Di Guglielmo, F. Fummi, M. Jenihhin, G. Pravadelli, J. Raik, R. Ubar
"On the Combined Use of HLDDs and EFSMs for Functional ATPG"
Proceedings of IEEE East-West Design and Test International Symposium, Yerevan, Armenia, 2007

P. Destro, F. Fummi, G. Pravadelli,
"A Smooth Refinement Flow for Co-designing HW and SW Threads",
Proceedings of ACM/IEEE Design, Automation and Test in Europe (DATE),
Acropolis, Nice, France, 16-20 April, 2007

N. Bombieri, F. Fummi, G. Pravadelli,
"Incremental ABV for Functional Validation of TL-to-RTL Design Refinement",
Proceedings of "ACM/IEEE Design, Automation and Test in Europe (DATE)",
Acropolis, Nice, France, 16-20 April, 2007

Jaan Raik, Raimund Ubar, Anna Krivenko, Margus Kruus,
"Hierarchical Identification of Untestable Faults in Sequential Circuits",
Proceedings of the 10th IEEE Euromicro Conference on Digital Systems Design DSD2007, IEEE Computer Society,27-31 August 2007, Lübeck, Germany, pp. 668-671

 

2006

N. Bombieri, F. Fummi, G. Pravadelli,
"A Methodology for Abstracting RTL Designs into TL Descriptions",
Proceedings of ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE),
Napa Valley, CA, USA, 27-29 July, 2006

N. Bombieri, F. Fummi, G. Pravadelli,
"Incremental ABV for TL-to-RTL Design Refinement",
Poceedings of IEEE East-West Design & Test International Workshop (EWDTW),
Sochi (Russia), September 15-19, 2006

N. Bombieri, F. Fummi.,
"On the Automatic Transactor Generation in TLM-based Design Flows",
Poceedings of IEEE International High Level Design Validation and Test Workshop (HLDVT), Monterey, CA, USA, 8-10 November, 2006

Kullmann, O., Lynce, I. and Marques-Silva, J.
"Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable
sub-clause-sets and the lean kernel",
Proceedings of International Conference on Theory and Applications of Satisfiability
Testing, Seattle, USA, 2006

Morgado, A., Matos, P., Manquinho, V. and Marques-Silva, J.
"Counting Models in Integer Domains",
Proceedings of International Conference on Theory and Applications of Satisfiability
Testing, Seattle, USA, 2006

D. Karlsson, P. Eles, Z. Peng,
"Formal Verification of Component-based Designs",
in Design Automation for Embedded Systems, 2006

Manquinho, V. and Marques-Silva, J.
"On Using Cutting Planes in Pseudo-Boolean Optimization",
Journal on Satisfiability, Boolean Modeling

Jaan Raik, Raimund Ubar, Taavi Viilukas,
" High-Level Decision Diagram based Fault Models for Targeting FSMs",
Proceedings of the 9th IEEE Euromicro Conference on Digital Systems Design DSD2006, Cavtat, Aug. 31- Sep. 2, 2006, pp. 353-358


Deliverables