In this page you will find documents and tools publicly available for download.

Table of Contents

• Publications 2008
• Publications 2009
• Publications 2010
• Deliverables

Publications 2008

N. Yevtushenko, S. Tikhomirova, T. Villa: A new algorithm to solve synchronous FSM equations.
Proc. of International Workshop on Logic and Synthesis (IWLS), 2008, pp. 72-78

D. Bresolin , A. Montanari , P. Sala , G. Sciavicco: Optimal tableaux for Right Propositional Neighborhood Logic over Linear Orders.
Proc. of European Conference on Logics in Artificial Intelligence (ECLAI), 2008, Springer, pp. 62-75

D. Bresolin , A. Montanari , P. Sala: Optimal tableau for Right Propositional Neighborhood Logic over trees.
Proc. of IEEE International Symposium on Temporal Representation and Reasoning (TIME), 2008, pp. 110-117

L. Benvenuti, D. Bresolin, A. Casagrande, P. Collins, A. Ferrari, E. Mazzi, A. Sangiovanni-Vincentelli and T. Villa: Reachability computation for hybrid systems with Ariadne.
Proc. of IFAC World Congress 2008, pp. 8960-8965

G. Di Guglielmo, F. Fummi, M. Hampton, G. Pravadelli, F. Stefanni: The Role of Parallel Simulation in Functional Verification.
Proc. of IEEE International High Level Design Validation and Test Workshop (HLDVT) 2008 , pp. 117-124

H. Zabel, W. Mueller: Präzises Interrupt Scheduling in abstrakten RTOS Modellen in SystemC.
Proc. of Workshop on Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und System, 2008

H. Zabel, W. Mueller: An Efficient Time Annotation Technique in Abstract RTOS Simulations for Multiprocessor Task Migration.
Proc. of IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES), 2008, pp. 181-190

J. Marques-Silva, and J. Planes: Algorithms for Maximum Satisfiability using Unsatisfiable Cores.
Proc. of ACM/IEEE Design, Automation and Test in Europe Conference and Exhibition(DATE), 2008, pp. 408-413

J. Marques-Silva: Model Checking with Boolean Satisfiability.
In Journal of Algorithms in Cognition, Informatics and Logic, 2008, vol. 63, no. 1-3, pp. 3-16

J. Marques-Silva: Practical Applications of Boolean Satisfiability.
Proc. of IEEE International Workshop on Discrete Event Systems (WODES), 2008, pp. 74-80

J. Marques-Silva, and V. Manquinho: Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms.
Proc. of International Conference on Theory and Applications of Satisfiability Testing (SAT), 2008, pp. 225-230

A. Cimatti, M. Roveri and S. Tonetta: Symbolic compilation of PSL.
In IEEE Transactions on Computer-Aided-Design of Intergated Circuits and Systems, vol. 27, no. 10, 2008

K. Greimel, R. Bloem. B. Jobstmann, and M. Vardi: Open Implication.
Proc. of International Colloquium on Automata, Languages and Programming (ICALP'08), 2008, vol. 5126, pp. 361-372

R. Tögl, G. Hofferek, K. Greimel, A. Leung, R. C-W. Phan, R. Bloem: Formal Analysis of a TPM-Based Secrets Distribution and Storage Scheme.
Proc. of the International Symposium on Trusted Computing (TrustCom), 2008

L. Di Guglielmo, F. Fummi and G. Pravadelli: Vacuity Analysis by Fault Simulation.
Proc. of ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE), 2008, pp. 27-36

A. Cimatti, L. Palopoli, Y. Ramadia: Symbolic Computation of Schedulability Regions Using Parametric Timed Automata.
Proc. of IEEE Real-Time Systems Symposium (RTSS), 2008, pp. 80-89

G. Di Guglielmo: On the validation of embedded systems through functional ATPG.
Proc. of IEEE Ph.D. Research in Microelectronics and Electronics (PRIME), 2008, pp. 149-152

P. Matos, J. Planes, F. Letombe, J. Marques-Silva: A MAX-SAT Algorithm Portfolio.
Proc. of European Conference on Artificial Intelligence (ECAI), 2008, pp. 911-912

J. Marques-Silva, I. Lynce, V. Manquinho: Symmetry Breaking for Maximum Satisfiability.
Proc. of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2008, pp. 1-15

F. Letombe, J. Marques-Silva: Improvements to Hybrid Incremental SAT Algorithms.
Proc. of International Conference on Theory and Applications of Satisfability Testing (SAT), 2008, pp. 168-181

F. Heras, V. Manquinho, J. Marques-Silva: On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization.
Proc. of The Florida Artificial Intelligence Research Society Conference (FLAIRS), 2008, pp. 71-76

I. Lynce, V. Manquinho, J. Marques-Silva: Backtracking.
In Wiley Encyclopedia of Computer Science and Engineering, 2008

Publications 2009

M. Liffiton, M. Mneimneh, I. Lynce, Z. Andraus, J. Marques-Silva, and K. Sakallah: A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas.
In Constraints , 2009, vol. 14, no. 4, pp. 415-442

H. Chen and J. Marques-Silva: TG-PRO: A New Model for SAT-Based ATPG.
Proc. of IEEE High Level Design Validation and Test Workshop (HLDVT), 2009, pp. 76-81

L. Cordeiro, B. Fischer and J. Marques-Silva: SMT-Based Bounded Model Checking for Embedded ANSI-C Software.
Proc. of International Conference on Automated Software Engineering (ASE), 2009, pp. 137-148

J. Argelich, I. Lynce and J. Marques-Silva: On Solving Boolean Multilevel Optimization Problems.
Proc. of International Joint Conference on Artificial Intelligence (IJCAI), 2009, pp. 393-398

V. Manquinho, J. Marques-Silva and J. Planes: Algorithms for Weighted Boolean Optimization.
Proc. of International Conference on Theory and Applications of Satisfability Testing (SAT), 2009, pp. 495-508

Y. Chen, S. Safarpour, A. Veneris and J. Marques-Silva: Spatial and temporal design debug using partial MaxSAT.
Proc. of Great Lakes Symposium on VLSI (GLSVLSI), 2009, pp. 345-350

L. Cordeiro, B. Fischer, H. Chen and J. Marques-Silva: Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints.
Proc. of International Conference on Embedded Software and Systems (ICESS), 2009

R. Bloem, K. Chatterjee, T. A. Henzinger, B. Jobstmann: Better Quality in Synthesis through Quantitative Objectives.
Proc. of International Conference on Computer Aided Verification (CAV), 2009, pp. 140-156

A. Cimatti, M. Roveri, S. Tonetta: Requirements Validation for Hybrid Systems.
Proc. of International Conference on Computer Aided Verification (CAV), 2009, pp. 188-203

A. Cimatti, A. Griggio, R. Sebastiani: Interpolant Generation for UTVPI.
Proc. of International Conference on Automated Deduction (CADE), 2009, pp. 167-182

N. Bombieri, F. Fummi, G. Pravadelli, M. Hampton, F. Letombe: Functional qualification of TLM verification.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2009 , pp. 190-195

D. Bresolin, G. Di Guglielmo, F. Fummi, G. Pravadelli, T. Villa: The impact of EFSM composition on functional ATPG.
Proc. of IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS), 2009 , pp. 44-49

N. Bombieri, F. Fummi, G. Pravadelli, S. Vinco: Correct-by-construction generation of device drivers based on RTL testbenches.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2009, pp. 1500-1505

F. Fummi, G. Pravadelli, L. Di Guglielmo: The Role of Mutation Analysis for Property Qualification.
Proc of ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2009, pp. 28-35

D. Bresolin, V. Goranko, A. Montanari and G. Sciavicco: Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions.
Annals of Pure and Applied Logic (2009), doi: 10.1016/j.apal.2009.07.003

D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco: Undecidability of Interval Temporal Logics with the Overlap Modality.
Proc. of IEEE International Symposium on Temporal Representation and Reasoning (TIME), 2009, pp. 88-95

M. Becker, H. Zabel, W. Mueller, U. Kiffmeier: Integration abstrakter RTOS-Simulation in den Entwurf eingebetteter automobiler E/E-Systeme.
Proc. of Workshop on Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2009

H. Zabel, W. Mueller: Increased Accuracy through Noise Injection in Abstract RTOS Simulation.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2009, pp. 1632-1637

H. Zabel, W. Mueller, A. Gerstlauer: Accurate RTOS Modelling and Analysis with SystemC.
In: W. Ecker, W. Mueller, R. Doemer (eds.) "Hardware Dependent Software - Principles and Practice", Springer Verlag, Dordrecht, 2009

W.Ecker, W. Mueller, R. Doemer: Hardware-dependent Software - Introduction and Overview.
In: W. Ecker, W. Mueller, R. Doemer (eds.) "Hardware Dependent Software - Principles and Practice", Springer Verlag, Dordrecht, 2009

A. Darbari, B. Fischer and J. Marques-Silva: Formalizing a SAT Proof Checker in Coq.
Proc. of Coq Workshop, 2009

V. Bushkov, and N. Yevtushenko and T. Villa: Discussion on supervisory control by solving automata equations.
Proc. of East-West Design and Test Symposium (EWDTS), 2009, pp. 77-79

R. Könighofer, G. Hofferek, R. Bloem: Debugging Formal Specifications Using Simple Counterstrategies.
Proc. of Formal Methods in Computer Aided Design (FMCAD), 2009

D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu and R. Sebastiani: Software Model Checking via Large-Block Encoding.
Proc. of Formal Methods in Computer Aided Design (FMCAD), 2009

A. Cimatti, J. Dubrovin, T. Junttila and M. Roveri: Structure-Aware Computation of Predicate Abstraction.
Proc. of Formal Methods in Computer Aided Design (FMCAD), 2009

R. Bloem, K. Greimel, T. Henzinger, B. Jobstmann: Synthesizing Robust Systems.
Proc. of Formal Methods in Computer Aided Design (FMCAD), 2009

G. Di Guglielmo, F. Fummi, C. Marconcini, G. Pravadelli: Test generation based on CLP.
in K. Takahata (ed.) "Micro Electronic and Mechanical Systems", Intech, 2009

P. Matos and B. Fischer and J. Marques-Silva: A Lazy Unbounded Model Checker for Event-B.
Proc. of International Conference on Formal Engineering Methods (ICFEM), 2009, pp. 485-503

I. Lynce and J. Marques-Silva: Restoring CSP Satisfiability with MaxSAT.
Proc. of Portuguese Conference on Artificial Intelligence (EPIA), 2009.

N.Bombieri, F.Fummi and G. Pravadelli: On the Mutation Analysis of SystemC TLM-2.0 Standard.
Proc. of Microprocessor Test and Verification (MTV), 2009.

G. Di Guglielmo, F. Fummi, M. Hampton, F. Letombe, G. Pravadelli: On the Functional Qualification of a Platform Model.
Proc. of IEEE International Symposium on Defect and Fault Tollerance in VLSI Systems (DFTS), 2009, pp. 182-190

A. Acquaviva, N. Bombieri, F. Fummi, S. Vinco: Automatic Customization Of Device Drivers For IP-Cores Used With Assorted CPU Organization.
Proc. of ACM/IEEE International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), 2009.

A. Petrenko, N. Yevtushenko, T. Villa: Testing in Contest and Synthesis of the Unknown Component: Two Faces of the Same Coin.
Proc. of International Workshop on Logic and Synthesis (IWLS), 2009, pp. 96-101

J. Marques-Silva, I. Lynce, S. Malik: Conflict-Driven Clause Learning SAT Solvers.
In Handbook of Satisfiability, 2009, pp. 131-153

J. Marques-Silva: Boolean Satisfiability and EDA Applications.
In Practical Design Verification (Cambridge University Press), 2009

D. Bresolin, T. Villa: Assume-guarantee verifcation of hybrid systems in Ariadne (extended abstract).
Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES), 2009.

Publications 2010

M. Becker, T. Xie and W. Mueller, G. Di Guglielmo, G. Pravadelli and F. Fummi: RTOS-Aware Refinement for TLM2.0-Based Hw/Sw Designs.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2010.

L. Di Guglielmo, G. Pravadelli and F. Fummi: Vacuity Analysis for Property Qualification by Mutation of Checkers.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2010.

A. Cimatti, A. Franzen, K. Kalyanasundaram, M. Roveri and A. Griggio: Tighter Integration of BDD and SMT for Predicate Abstraction.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2010.

H. Hantson, J. Raik, M. Jenihhin, A. Chepurov, R. Ubar, G. Di Guglielmo, F. Fummi: Mutation Analysis with High-Level Decision Diagrams.
Proc. of IEEE Latin-American Test Workshop(LATW), 2010.

G. Di Guglielmo, F. Fummi, G. Pravadelli, S. Soffia, M. Roveri: Semi-Formal Functional Verification by EFSM traversing via NuSMV.
Proc. of IEEE International High Level Design Validation and Test Workshop (HLDVT), 2010.

R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. Könighofer, M. Roveri, V. Schuppan, R. Seeber: RATSY - A new Requirements Analysis Tool with Synthesis.
Proc. of Computer Aided Verification(CAV), 2010 (to appear).

R. Bloem, K. Chatterjee, K. Greimel, T. Henzinger, B. Jobstmann: Robustness in the Presence of Liveness.
Proc. Computer Aided Verification(CAV), 2010 (to appear).

N. Bombieri, F. Fummi, G. Pravadelli: ABSTRACTION OF RTL IPs INTO EMBEDDED SOFTWARE.
Proc. of ACM/IEEE Design Automation Conference (DAC), 2010.

N. Bombieri, F. Fummi, V. Guarnieri: AUTOMATIC SYNTHESIS OF OSCI TLM-2.0 MODELS INTO RTL BUS-BASED IPS.
Proc. of IEEE International High Level Design Validation and Test Workshop (HLDVT), 2010.

T. Xie, W. Müller, F. Letombe: Efficient Mutation-Analysis Coverage for Constrained Random Verification.
Proc. of The IFIP 21st World Computer Congress, TC10 Working Conference on Distributed and Parallel Embedded Systems (DIPES), 2010 (to appear).

A. Cimatti, A. Franzen, A. Griggio, R. Sebastiani, C. Stenico: Satisfiability Modulo the Theory of Costs: Foundations and Applications.
Proc. of Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2010 (to appear).

A. Cimatti, A. Griggio, R. Sebastiani: Efficient Interpolant Generation in Satisfiability Modulo Theory.
To appear in ACM Transactions on Computational Logic (TOCL), 2010 (to appear).

M. Oliveira, H. Zabel, and W. Mueller: Assertion-Based Verification of RTOS Properties.
Proc. of ACM/IEEE Design, Automation and Test in Europe (DATE), 2010.

W. Mueller, M.Oliveira, H. Zabel, and M. Becker: Verification of Real-Time Properties for Hardware-Dependant Software.
Proc. of IEEE International High-Level Design Validation and Test Workshop (HLDVT), 2010.

M. Becker, H. Zabel, and W. Müller: A Mixed Level Simulation Environment for Stepwise RTOS Software Refinement.
Proc. of IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES), 2010.

A. Darbari, B. Fischer, J. Marques-Silva: Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking.
Proc. of International Colloquium On Theoretical Aspects Of Computing(ICTAC), 2010.

J. Marques-Silva, M. Janota, I. Lynce: On Computing Backbones of Propositional Theories.
Proc. of European Conference On Artificial Intelligence(ECAI), 2010.

J. Marques-Silva: Minimal Unsatisfiability: Models, Algorithms & Applications.
Proc. of International Symposium On Multiple-Valued Logic (ISMVL), 2010.

L. Cordeiro, B. Fischer, J. Marques-Silva: Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking.
Proc. of Engineering of Computer-Based Systems (ECBS), 2010, pp. 160-169.

M. Janota, G. Botterweck, R. Grigore, J. Marques-Silva: How to Complete an Interactive Configuration Process?
Proc. of Software Seminar (SOFSEM), 2010, pp. 528-539

J. Argelich, D. Le Berre, I. Lynce, J. Marques-Silva, P. Rapicault: Solving Linux Upgradeability Problems Using Boolean Optimization.
Proc. of Logics For Component Configuration(LOCOCO), 2010.

J. Marques-Silva, J. Argelich, A. Graca, I. Lynce: Boolean Lexicographic Optimization.
Proc. of Knowledge Representation And Automated Reasoning(RCRA), 2010.

Y. Chen, S. Safarpour, J. Marques-Silva, A. Veneris: Automated Design Debugging with Maximum Satisfiability.
In IEEE Transactions on computer-aided design: In press, 2010.

N. Bombieri, G. Di Guglielmo, L. Di Guglielmo, M. Ferrari, F. Fummi, G. Pravadelli, F. Stefanni, A. Venturelli: HIFSuite: Tools for HDL Code Conversion and Manipulation.
Proc. of IEEE High Level Design Validation and Test Workshop (HLDVT), 2010.

J. Marques-Silva, J. Planed: Algorithms for Maximum Satisfability using Unsatisfable Cores.
Advances in Logic Synthesis. In press (2010).

M. Janota, R. Grigore, J. Marques-Silva: Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription.
Proc. of European Conference on Logics in Artificial Intelligence (JELIA), 2010.

A. Cimatti, S. Mover, M. Roveri, S. Tonetta: From Sequential Extended Regular Expressions to NFA with Symbolic Labels.
Proc. of 15th International Conference on Implementation and Application of Automata Winnipeg (CIAA), 2010.

L. Bu, A. Cimatti, X. Li, S. Mover, S. Tonetta: Model Checking of Hybrid Systems using Shallow Synchronization.
Proc. of IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS + FORTE),2010.

A. Bernasconi, V. Ciriani, G. Trucco, T. Villa: Logic synthesis by signal-driven decomposition, in Hardware Acceleration of EDA Algorithms: Custom ICs, FPGAs and GPUs.
In K. Gulati and S.P. Khatri eds. Springer, 2010 (invited chapter).

M. Bertasi, G. Di Guglielmo, F. Fummi, G. Pravadelli: Effective EFSM generation for HW/SW-design verification.
Proc. of IEEE Biennial Baltic Electronics Conference (BEC), 2010.

N. Bombieri, F. Fummi, V. Guarnieri: Model Checking on TLM-2.0 IPs through automatic TLM-to-RTL Synthesis.
Proc. of IEEE/IFIP International Conference on VLSI and System on Chip (VLSI-Soc), 2010 (to appear).

Deliverables

• D1.1 - Definition of the modelling and verification requirements and COCONUT flow
• D1.2 - Revision of the modelling and verification requirements and COCONUT flow
• D2.1 - State of the Art and Objectives on Property Validation and Synthesis of System Specification
• D2.2 - Techniques, tools and methodologies for property validation and synthesis of system specification
• D2.3 - Tools for property validation and synthesis of system specification
• D3.1 - State of the art and objectives on correct-by-construction TLM modelling
• D3.2 - Techniques, tools and methodologies for correct-by-construction TLM modelling
• D3.3 - Tools for correct-by- construction TLM modelling
• D4.1 - State of the art and objectives on post-refinement verification
• D4.2 - Techniques, tools and methodologies for post-refinement verification
• D4.3 - Tools for post-refinement verification
• D5.1 - TLM modelling of the platform and first phase of validation of the COCONUT flow
• D5.2 - Mapping of the application design on the TLM platform
• D5.3 - Final validation of COCONUT flow and tool integration
• D6.1 - Project presentation and COCONUT web site
• D6.2 - Dissemination and use plan
• D6.3 - Plan for the use and dissemination of foreground
• D7.1 - Final report