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

Table of Contents

 

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 (ISTRR), 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

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: An International Journal, August 2008

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, 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

Publications 2009

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

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

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

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

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

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

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

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, pp. 396-403

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.
To appear in FMCAD 2009

D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu and R. Sebastiani: Software Model Checking via Large-Block Encoding.
To appear in FMCAD 2009

A. Cimatti, J. Dubrovin, T. Junttila and M. Roveri: Structure-Aware Computation of Predicate Abstraction.
To appear in FMCAD 2009

R. Bloem, K. Greimel, T. Henzinger, B. Jobstmann: Synthesizing Robust Systems.
To appear in FMCAD 2009

G. Di Guglielmo, F. Fummi, C. Marconcini, G. Pravadelli: Test generation based on CLP.
To appear in MEMS

P. Matos and B. Fischer and J. Marques-Silva: A Lazy Unbounded Model Checker for Event-B.
To appear in ICFEM 2009.

I. Lynce and J. Marques-Silva: Restoring CSP Satisfiability with MaxSAT.
To appear in EPIA 2009.

N.Bombieri, F.Fummi and G. Pravadelli: On the Mutation Analysis of SystemC TLM-2.0 Standard.
To appear in MTV 2009.

M. Janota, G. Botterweck, R. Grigore, J. Marques-Silva: How to Complete an Interactive Configuration Process? -- Configuring as Shopping.
To appear in SofSem 2010.

 

Deliverables

  • D1.1 - Definition 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
  • 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
  • D4.1 - State of the art and objectives on post-refinement verification
  • D4.2 - Techniques, tools and methodologies for post-refinement verification
  • D5.1 - TLM modelling of the platform and first phase of validation of the COCONUT flow
  • D6.1 - Project presentation and COCONUT web site
  • D6.2 - Dissemination and use plan