GAL: Towards Large Simulations with Tens of Agents. - Cyril Brom; Ondrej Sery; Tomás Poch; Pavel Safrata (IVA, 2005)

Level-of-Detail in Behaviour of Virtual Humans. - Ondrej Sery; Tomás Poch; Pavel Safrata; Cyril Brom (SOFSEM, 2006)

Slicing of Component Behavior Specification with Respect to Their Composition. - Ondrej Sery; Frantisek Plásil (CBSE, 2007)

CoCoME in Fractal. - Lubomír Bulej; Tomás Bures; Thierry Coupaye; Martin Decký; Pavel Jezek; Pavel Parízek; Frantisek Plásil; Tomás Poch; Nicolas Rivierre; Ondrej Sery; Petr Tuma 001 (CoCoME, 2007)

CoCoME in SOFA. - Tomás Bures; Martin Decký; Petr Hnetynka; Jan Kofron; Pavel Parízek; Frantisek Plásil; Tomás Poch; Ondrej Sery; Petr Tuma 001 (CoCoME, 2007)

Simulation Level of Detail for Virtual Humans. - Cyril Brom; Ondrej Sery; Tomás Poch (IVA, 2007)

Making Components Fit: SPINing. - Jan Kofron; Tomás Poch; Ondrej Sery (SEW, 2008)

TBP: Code-Oriented Component Behavior Specification. - Jan Kofron; Tomás Poch; Ondrej Sery (SEW, 2008)

UnitCheck: Unit Testing and Model Checking Combined. - Michal Kebrt; Ondrej Sery (ATVA, 2009)

Applicability of the BLAST Model Checker: An Industrial Case Study. - Emanuel Kolb; Ondrej Sery; Roland Weiss (Ershov Memorial Conference, 2009)

Enhanced Property Specification and Verification in BLAST. - Ondrej Sery (FASE, 2009)

On Teaching Formal Methods: Behavior Models and Code Analysis. - Jan Kofron; Pavel Parízek; Ondrej Sery (TFM, 2009)

Modes in component behavior specification via EBP and their application in product lines. - Jan Kofron; Frantisek Plásil; Ondrej Sery (Inf. Softw. Technol., 2009)

Strengthening Component Architectures by Modeling Fine-Grained Entities. - Tomás Bures; Pavel Jezek; Michal Malohlava; Tomás Poch; Ondrej Sery (EUROMICRO-SEAA, 2011)

Function Summaries in Software Upgrade Checking. - Grigory Fedyukovich; Ondrej Sery; Natasha Sharygina (Haifa Verification Conference, 2011)

Interpolation-Based Function Summaries in Bounded Model Checking. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (Haifa Verification Conference, 2011)

FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (ATVA, 2012)

Leveraging Interpolant Strength in Model Checking. - Simone Fulvio Rollini; Ondrej Sery; Natasha Sharygina (CAV, 2012)

Incremental upgrade checking by means of interpolation-based function summaries. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (FMCAD, 2012)

PINCETTE - Validating Changes and Upgrades in Networked Software. - Hana Chockler; Giovanni Denaro; Meijia Ling; Grigory Fedyukovich; Antti Eero Johannes Hyvärinen; Leonardo Mariani; Ali Muhammad; Manuel Oriol; Ajitha Rajan; Ondrej Sery; Natasha Sharygina; Michael Tautschnig (CSMR, 2013)

eVolCheck: Incremental Upgrade Checker for C. - Grigory Fedyukovich; Ondrej Sery; Natasha Sharygina (TACAS, 2013)

Threaded behavior protocols. - Tomás Poch; Ondrej Sery; Frantisek Plásil; Jan Kofron (Formal Aspects Comput., 2013)

Function Summarization-Based Bounded Model Checking. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (Validation of Evolving Software, 2015)

Incremental Upgrade Checking. - Ondrej Sery; Grigory Fedyukovich; Natasha Sharygina (Validation of Evolving Software, 2015)

Flexible SAT-based framework for incremental bounded upgrade checking. - Grigory Fedyukovich; Ondrej Sery; Natasha Sharygina (Int. J. Softw. Tools Technol. Transf., 2017)