You are here

Silvio Ranise

Head of Unit
  • Phone: 0461314192
  • FBK Povo
Short bio

Silvio Ranise received his Ms. Eng. in 1997 at the University of Genova (Italy) and his PhD in Computer Engineering from the University of Genova (Italy) and the University H. Poincare ́ (Nancy, France) in 2002 in the context of a joint PhD program between Italy and France. He works at FBK in the S&T Research Unit as Senior Researcher since April 2010. His previous appointments are: assistant professor at the U. H. Poincare ́ in 2001-2002, INRIA researcher at the LORIA computer science laboratory of Nancy in 2002-2008, research associate at the University of Verona (in the context of the EU Project AVANTSSAR) in 2008-2010, visiting professor at the Department of Computer Science of the University of Milano. His research focuses on formal methods for the automatic analysis of security-sensitive applications and he has published more than 65 papers in international conferences and journals on automated analysis of security policies, infinite state model checking, and Satisfiability Modulo Theories (SMT) solving. He has been initiator and co-ordinator of the SMT-Lib initiative, and started the SMT workshop series on SMT techniques. He has also given tutorials on SMT and infinite state model checking techniques at international conferences. In 2010, he received the HVC award for his “pivotal and continuous role in building and promoting the SMT community.” 

Publications
  1. D. Déharbe; P. Fontaine; S. Ranise; C Ringeissen,
    Decision Procedures for the Formal Analysis of Software,
    2006
    , (Theoretical Aspects of Computing - ICTAC 2006,
    Tunis, Tunisia,
    11/20/2006 a 11/24/2006)
  2. M. P. Bonacina; S. Ghilardi; E. Nicolini; S. Ranise; D Zucchelli,
    Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures,
    2006
    , (Automated Reasoning Third International Joint Conference, IJCAR 2006,
    Seattle, WA, USA,
    08/17/2006 a 08/20/2006)
  3. H. Kirchner; S. Ranise; C. Ringeissen; D. K. Tran,
    Automatic Combinability of Rewriting-Based Satisfiability Procedures,
    2006
    , (Logic for Programming, Artificial Intelligence, and Reasoning 13th International Conference, LPAR 2006,
    Phnom Penh, Cambodia,
    11/13/2006 a 11/17/2006)
  4. S. Ranise; C. G. Zarba,
    A Theory of Singly-Linked Lists and its Extensible Decision Procedure,
    2006
    , (Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006),
    Pune, India,
    09/11/2006 a 09/15/2006)
  5. Armando A.; Compagna L.; Ranise S.,
    Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation,
    Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of his 60th Birthday,
    Berlin,
    Springer-Verlag,
    2005
    , pp. 30 -
    45
  6. A. Armando; L. Compagna; S. Ranise,
    Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation,
    Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday,
    Berlin Heidelberg,
    Springer,
    2005
    , pp. 30 -
    45
  7. Armando A.; Bonacina M. P.; Ranise S.; Schulz S.,
    On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal,
    in «LECTURE NOTES IN COMPUTER SCIENCE»
    vol.3717,
    2005
    , pp. 65-
    80
    , (Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005,
    Vienna, Austria,
    19-21/09/2005)
  8. H. Kirchner; S. Ranise; C. Ringeissen and D. K. Tran,
    On Superposition-Based Satisfiability Procedures and Their Combination,
    2005
    , (Theoretical Aspects of Computing – ICTAC 2005,
    Hanoi, Vietnam,
    10/17/2005 a 10/21/2005)
  9. S. Ranise; C. Ringeissen; C. G. Zarba,
    Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic,
    2005
    , (Frontiers of Combining Systems,
    Vienna, Austria,
    09/19/2005 a 09/21/2005)
  10. P. Fontaine; S. Ranise; C. G. Zarba,
    Combining Lists with Non-stably Infinite Theories,
    2005
    , (Logic for Programming, Artificial Intelligence, and Reasoning 11th International Conference, LPAR 2004,
    Montevideo, Uruguay,
    03/14/2005 a 03/18/2005)

Pages