| 2025 | IFM | CTL Model Checking Partially Specified Systems. | Eshita Zaman, Christopher Johannsen, Andrew S. Miner, Gianfranco Ciardo, Samik Basu |
| 2024 | DAC | RexBDDs: Reduction-on-Edge Complement-and-Swap Binary Decision Diagrams. | Gianfranco Ciardo, Andrew S. Miner, Lichuan Deng, Junaid Babar |
| 2024 | ECAI | Comparing Lossless Compression Methods for Chess Endgame Data. | Dave Gomboc, Christian R. Shelton, Andrew S. Miner, Gianfranco Ciardo |
| 2022 | IFM | HyperPCTL Model Checking by Probabilistic Decomposition. | Eshita Zaman, Gianfranco Ciardo, Erika brahm, Borzoo Bonakdarpour |
| 2022 | TAP | Bddl: A Type System for Binary Decision Diagrams. | Yousra Lembachar, Ryan Rusich, Iulian Neamtiu, Gianfranco Ciardo |
| 2019 | TACAS | Presentation of the 9th Edition of the Model Checking Contest. | Elvio Gilberto Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal-Zilio, Francesco Gall, Lom-Messan Hillah, Francis Hulin-Hubard, Peter Gjl Jensen, Log Jezequel, Fabrice Kordon, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Andrew S. Miner, Emmanuel Paviot-Adet, Jir Srba, Yann Thierry-Mieg, Tom van Dijk, Karsten Wolf |
| 2019 | TACAS | i _\mathrm Rank : A Variable Order Metric for DEDS Subject to Linear Invariants. | Elvio Gilberto Amparore, Gianfranco Ciardo, Susanna Donatelli, Andrew S. Miner |
| 2019 | TACAS | Binary Decision Diagrams with Edge-Specified Reductions. | Junaid Babar, Chuan Jiang, Gianfranco Ciardo, Andrew S. Miner |
| 2018 | LPAR | Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse. | Chuan Jiang, Gianfranco Ciardo |
| 2018 | TACAS | Generation of Minimum Tree-Like Witnesses for Existential CTL. | Chuan Jiang, Gianfranco Ciardo |
| 2015 | WABI | Scrible: Ultra-Accurate Error-Correction of Pooled Sequenced Reads. | Denise Duma, Francesca Cordero, Marco Beccuti, Gianfranco Ciardo, Timothy J. Close, Stefano Lonardi |
| 2014 | SPIRE | Sequence Decision Diagrams. | Hind Alhakami, Gianfranco Ciardo, Marek Chrobak |
| 2013 | WABI | Accurate Decoding of Pooled Sequenced Data Using Compressed Sensing. | Denisa Duma, Mary Wootters, Anna C. Gilbert, Hung Q. Ngo, Atri Rudra, Matthew Alpert, Timothy J. Close, Gianfranco Ciardo, Stefano Lonardi |
| 2011 | ATVA | Symbolic Verification and Test Generation for a Network of Communicating FSMs. | Xiaoqing Jin, Gianfranco Ciardo, Tae-Hyong Kim, Yang Zhao |
| 2011 | TASE | A Symbolic Algorithm for Shortest EG Witness Generation. | Yang Zhao, Xiaoqing Jin, Gianfranco Ciardo |
| 2009 | ATVA | Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation. | Yang Zhao, Gianfranco Ciardo |
| 2009 | SOFSEM | Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams. | Min Wan, Gianfranco Ciardo |
| 2009 | SOFSEM | Symbolic Reachability Analysis of Integer Timed Petri Nets. | Min Wan, Gianfranco Ciardo |
| 2007 | CAV | Parallelising Symbolic State-Space Generators. | Jonathan Ezekiel, Gerald Lttgen, Gianfranco Ciardo |
| 2007 | TACAS | Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams. | Andy Jinqing Yu, Gianfranco Ciardo, Gerald Lttgen |
| 2006 | ATVA | A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis. | Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Yu |
| 2006 | TACAS | New Metrics for Static Variable Ordering in Decision Diagrams. | Radu Siminiceanu, Gianfranco Ciardo |
| 2003 | CAV | Structural Symbolic CTL Model Checking of Asynchronous Systems. | Gianfranco Ciardo, Radu Siminiceanu |
| 2003 | MASCOTS | Profit-driven Service Differentiation in Transient Environments. | Qi Zhang, Evgenia Smirni, Gianfranco Ciardo |
| 2003 | TACAS | Saturation Unbound. | Gianfranco Ciardo, Robert M. Marmorstein, Radu Siminiceanu |
| 2002 | DSN | SMART: Stochastic Model-checking Analyzer for Reliability and Timing. | Gianfranco Ciardo, R. L. Jones III, Robert M. Marmorstein, Andrew S. Miner, Radu Siminiceanu |
| 2002 | FMCAD | Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths. | Gianfranco Ciardo, Radu Siminiceanu |
| 2002 | ICDCS | ADAPTLOAD: Effective Balancing in Custered Web Servers Under Transient Load Conditions. | Alma Riska, Wei Sun, Evgenia Smirni, Gianfranco Ciardo |
| 2001 | TACAS | Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. | Gianfranco Ciardo, Gerald Lttgen, Radu Siminiceanu |
| 2000 | ICCCN | Characterizing temporal locality and its impact on web server performance. | Ludmila Cherkasova, Gianfranco Ciardo |
| 2000 | SIGMETRICS | Using the exact state space of a Markov model to compute approximate stationary measures. | Andrew S. Miner, Gianfranco Ciardo, Susanna Donatelli |
| 1996 | MASCOTS | Well-Defined Stochastic Petri Nets. | Gianfranco Ciardo, Robert Zijal |
| 1995 | SIGMETRICS | Modeling A Fibre Channel Switch with Stochastic Petri Nets. | Gianfranco Ciardo, Ludmila Cherkasova, Vadim E. Kotov, Tomas Rokicki |
| 1995 | SIGMETRICS | Non-Markovian Petri Nets (Panel). | Kishor S. Trivedi, Andrea Bobbio, Mikls Telek, Reinhard German, Gianfranco Ciardo, Antonio Puliafito |
| 1993 | ICRA | Performabilty Modeling of an Automated Manufacturing System with Deterministic and Stochastic Petri Nets. | Christoph Lindemann, Gianfranco Ciardo, Reinhard German, Gnter Hommel |
| 1993 | MASCOTS | SPNP: The Stochastic Petri Net Package (Version 3.1). | Gianfranco Ciardo, Kishor S. Trivedi |
| 1993 | MASCOTS | Modeling Using Stochastic Reward Nets. | Jogesh K. Muppala, Gianfranco Ciardo, Kishor S. Trivedi |
| 1993 | SIGMETRICS | Dependability and Performability Analysis. | Kishor S. Trivedi, Gianfranco Ciardo, Manish Malhotra, Robin A. Sahner |