| Object-oriented logical specification of time-critical systems A Morzenti, P San Pietro ACM Transactions on Software Engineering and Methodology (TOSEM) 3 (1), 56-98, 1994 | 112 | 1994 |
| A scalable formal method for design and automatic checking of user interfaces J Berstel, SC Reghizzi, G Roussel, PS Pietro ACM Transactions on Software Engineering and Methodology (TOSEM) 14 (2), 124-167, 2005 | 80 | 2005 |
| A scalable formal method for design and automatic checking of user interfaces J Berstel, S Crespi Reghizzi, G Roussel, P San Pietro ACM Transactions on Software Engineering and Methodology (TOSEM) 14 (2), 124-167, 2005 | 80 | 2005 |
| Embedding time granularity in a logical specification language for synchronous real-time systems E Ciapessoni, E Corsetti, A Montanari, P San Pietro Science of computer programming 20 (1-2), 141-171, 1993 | 67 | 1993 |
| The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties M Pradella, A Morzenti, P San Pietro Proceedings of the the 6th joint meeting of the European software …, 2007 | 53 | 2007 |
| A tool for deciding the satisfiability of continuous-time metric temporal logic MM Bersani, M Rossi, P San Pietro Acta Informatica 53 (2), 171-206, 2016 | 49 | 2016 |
| Bounded satisfiability checking of metric temporal logic specifications M PRADELLA, A MORZENTI, P SAN PIETRO ACM Transactions on Software Engineering and Methodology (TOSEM). To appear, 2012 | 49 | 2012 |
| The tale of SOLOIST: a specification language for service compositions interactions D Bianculli, C Ghezzi, P San Pietro International Workshop on Formal Aspects of Component Software, 55-72, 2012 | 37 | 2012 |
| Refining real-time system specifications through bounded model-and satisfiability-checking M Pradella, A Morzenti, P San Pietro 2008 23rd IEEE/ACM International Conference on Automated Software …, 2008 | 37 | 2008 |
| Bounded reachability for temporal logic over constraint systems MM Bersani, A Frigeri, A Morzenti, M Pradella, M Rossi, P San Pietro 2010 17th International Symposium on Temporal Representation and Reasoning …, 2010 | 33 | 2010 |
| A Petri net and logic approach to the specification and verification of real time systems D Mandrioli, AC Morzenti, M Pezze, PSS San Pietro John Wiley & Sons, 1996 | 32 | 1996 |
| Dealing with different time scales in formal specifications E Corsetti, E Crivelli, D Mandrioli, A Montanari, AC Morzenti, P San Pietro, ... Proceedings of the Sixth International Workshop on Software Specification …, 1991 | 29 | 1991 |
| Practical model checking of LTL with past M Pradella, P San Pietro, P Spoletini, A Morzenti ATVA03: 1st Workshop on Automated Technology for Verification and Analysis, 2003 | 28 | 2003 |
| Picture languages: Tiling systems versus tile rewriting grammars A Cherubini, SC Reghizzi, M Pradella, P San Pietro Theoretical Computer Science 356 (1-2), 90-103, 2006 | 27 | 2006 |
| Model-checking TRIO specifications in SPIN A Morzenti, M Pradella, P San Pietro, P Spoletini International Symposium of Formal Methods Europe, 542-561, 2003 | 27 | 2003 |
| Liveness verification of reversal-bounded multicounter machines with a free counter Z Dang, OH Ibarra, P San Pietro International Conference on Foundations of Software Technology and …, 2001 | 24 | 2001 |
| A metric encoding for bounded model checking (extended version) M Pradella, A Morzenti, P San Pietro Arxiv preprint arXiv:0907.3085, 2009 | 21* | 2009 |
| Generation of execution sequences for modular time critical systems PS Pietro, A Morzenti, S Morasca IEEE Transactions on Software Engineering 26 (2), 128-149, 2000 | 21 | 2000 |
| Presburger liveness verification of discrete timed automata Z Dang, P San Pietro, RA Kemmerer Theoretical Computer Science 299 (1-3), 413-438, 2003 | 20 | 2003 |
| Presburger liveness verification of discrete timed automata Z Dang, P San Pietro, RA Kemmerer Theoretical Computer Science 299 (1-3), 413-438, 2003 | 20 | 2003 |
Matteo Pradellaassociate professor, Politecnico di MilanoEmail verificata su polimi.it
