Jiri Barnat

Vladimír Chlup

Proceedings of the 19th IEEE International Conference on Automation Science and Engineering, 2023

RoFIOS - Flexible Full-Stack Software Solution for Metamorphic Robots.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Conference on Automation Science and Engineering, 2023

2022

DivSIM , an interactive simulator for LLVM bitcode.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2022

2021

Reproducible execution of POSIX programs with DiOS.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2021

Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way?

[BibT_eX]

[DOI]

Martin Jonás

Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems, 2021

2020

On Symbolic Execution of Decompiled Programs.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE International Conference on Software Quality, 2020

2019

Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Local Nontermination Detection for Parallel C++ Programs.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 17th International Conference, 2019

RoFICoM - First Open-Hardware Connector for Metamorphic Robots.

[BibT_eX]

[DOI]

Proceedings of the 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2019

A Simulator for LLVM Bitcode.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2019

2018

DiVM: Model checking with LLVM and graph memory.

[BibT_eX]

[DOI]

J. Syst. Softw., 2018

On clock-aware LTL parameter synthesis of timed automata.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2018

Symbolic Computation via Program Transformation.

[BibT_eX]

[DOI]

Henrich Lauko

Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

Model Checking of C++ Programs Under the x86-TSO Memory Model.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2018

Parallel Model Checking Algorithms for Linear-Time Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017

SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking.

[BibT_eX]

[DOI]

Martin Jonás

CoRR, 2017

DiVM: Model Checking with LLVM and Graph Memory.

[BibT_eX]

[DOI]

CoRR, 2017

Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

From Model Checking to Runtime Verification and Back.

[BibT_eX]

[DOI]

Katarína Kejstová

Proceedings of the Runtime Verification - 17th International Conference, 2017

Using Off-the-Shelf Exception Support Components in C++ Verification.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE International Conference on Software Quality, 2017

Detecting Attractors in Biological Models with Uncertain Parameters.

[BibT_eX]

[DOI]

Proceedings of the Computational Methods in Systems Biology, 2017

Model Checking of C and C++ with DIVINE 4.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

Control Explicit-Data Symbolic Model Checking.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2016

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories.

[BibT_eX]

[DOI]

Softw. Qual. J., 2016

Model checking C++ programs with exceptions.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2016

Analysing sanity of requirements for avionics systems.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2016

DIVINE: Explicit-State LTL Model Checker - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 23rd International Symposium, 2016

LTL Parameter Synthesis of Parametric Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

On verifying C++ programs with probabilities.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

Tunable Online MUS/MSS Enumeration.

[BibT_eX]

[DOI]

Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

Parametric Multi-step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components.

[BibT_eX]

[DOI]

Proceedings of the Euro-Par 2016: Parallel Processing Workshops, 2016

Optimal observation mode scheduling for systems under temporal constraints.

[BibT_eX]

[DOI]

Proceedings of the 2016 American Control Conference, 2016

2015

Analysing Sanity of Requirements for Avionics Systems (Preliminary Version).

[BibT_eX]

[DOI]

CoRR, 2015

Fast, Dynamically-Sized Concurrent Hash Table.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 22nd International Symposium, 2015

Quo Vadis Explicit-State Model Checking.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2015: Theory and Practice of Computer Science, 2015

Techniques for Memory-Efficient Model Checking of C and C++ Code.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 13th International Conference, 2015

Weak Memory Models as LLVM-to-LLVM Transformations.

[BibT_eX]

[DOI]

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2015

2014

Model Checking C++ with Exceptions.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014

LTL Model Checking of Parametric Timed Automata.

[BibT_eX]

[DOI]

CoRR, 2014

Model Checking Parallel Programs with Inputs.

[BibT_eX]

[DOI]

Proceedings of the 22nd Euromicro International Conference on Parallel, 2014

Context-Switch-Directed Verification in DIVINE.

[BibT_eX]

[DOI]

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2014

LTL Model Checking of LLVM Bitcode with Symbolic Data.

[BibT_eX]

[DOI]

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2014

On Clock-Aware LTL Properties of Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Temporal Verification of Simulink Diagrams.

[BibT_eX]

[DOI]

Proceedings of the 15th International IEEE Symposium on High-Assurance Systems Engineering, 2014

2013

Control Explicit---Data Symbolic Model Checking: An Introduction

[BibT_eX]

[DOI]

CoRR, 2013

Formal analysis of piecewise affine systems through formula-guided refinement.

[BibT_eX]

[DOI]

Autom., 2013

Improved State Space Reductions for LTL Model Checking of C and C++ Programs.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2013

Towards Verification of Ensemble-Based Component Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

DCCL: verification of component systems with ensembles.

[BibT_eX]

[DOI]

Proceedings of the CBSE'13, 2013

DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Application of Concurrency to System Design, 2013

2012

On Parameter Synthesis by Parallel Model Checking.

[BibT_eX]

[DOI]

IEEE ACM Trans. Comput. Biol. Bioinform., 2012

Temporal Logic Control of Discrete-Time Piecewise Affine Systems.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2012

On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2012

Designing fast LTL model checking algorithms for many-core GPUs.

[BibT_eX]

[DOI]

J. Parallel Distributed Comput., 2012

Distributed LTL Model Checking with Hash Compaction.

[BibT_eX]

[DOI]

Jan Havlícek

Proceedings of the Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling, 2012

Verification of Systems with Degradation.

[BibT_eX]

[DOI]

Jana Tumova

Comput. Informatics, 2012

Executing Model Checking Counterexamples in Simulink.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

Checking Sanity of Software Requirements.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2012

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2012

Attraction-based receding horizon path planning with temporal logic constraints.

[BibT_eX]

[DOI]

Proceedings of the 51th IEEE Conference on Decision and Control, 2012

2011

Flash memory efficient LTL model checking.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2011

Distributed Algorithms for SCC Decomposition.

[BibT_eX]

[DOI]

Jaco van de Pol

J. Log. Comput., 2011

Computing Optimal Cycle Mean in Parallel on CUDA

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Platform Dependent Verification: On Engineering Verification Tools for 21st Century

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Timed Automata Approach to Verification of Systems with Degradation.

[BibT_eX]

[DOI]

Jana Tumova

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2011

Computing Strongly Connected Components in Parallel on CUDA.

[BibT_eX]

[DOI]

Proceedings of the 25th IEEE International Symposium on Parallel and Distributed Processing, 2011

2010

Scalable shared memory LTL model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2010

High-performance analysis of biological systems dynamics with the DiVinE model checker.

[BibT_eX]

[DOI]

David Safránek

Briefings Bioinform., 2010

Parallel Partial Order Reduction with Topological Sort Proviso.

[BibT_eX]

[DOI]

Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

Employing Multiple CUDA Devices to Accelerate LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Conference on Parallel and Distributed Systems, 2010

A symbolic approach to controlling piecewise affine systems.

[BibT_eX]

[DOI]

Proceedings of the 49th IEEE Conference on Decision and Control, 2010

2009

On algorithmic analysis of transcriptional regulation by LTL model checking.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2009

DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking

[BibT_eX]

[DOI]

Milan Ceska

Proceedings of the Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation, 2009

BioDiVinE: A Framework for Parallel Analysis of Biological Models

[BibT_eX]

[DOI]

Proceedings of the Proceedings Second International Workshop on Computational Models for Cell Processes, 2009

Quantitative Model Checking of Systems with Degradation.

[BibT_eX]

[DOI]

Jana Tumova

Proceedings of the QEST 2009, 2009

Cluster-Based I/O-Efficient LTL Model Checking.

[BibT_eX]

[DOI]

Pavel Simecek

Proceedings of the ASE 2009, 2009

CUDA Accelerated LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE International Conference on Parallel and Distributed Systems, 2009

A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2009

2008

Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 2008

Squeeze All the Power Out of Your Hardware to Verify Your Software!.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, 2008

Can Flash Memory Help in Model Checking?

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2008

Local Quantitative LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2008

Efficient Large-Scale Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Distributed Verification and Grid Computing, 10.08. - 14.08.2008, 2008

DiVinE Multi-Core - A Parallel LTL Model-Checker.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

Shared Hash Tables in Parallel Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 2007

Improved Distributed Algorithms for SCC Decomposition.

[BibT_eX]

[DOI]

Jaco van de Pol

Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 2007

Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE.

[BibT_eX]

[DOI]

Proceedings of the First Workshop "From Biology To Concurrency and back", 2007

Tutorial: Parallel Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2007

Scalable Multi-core LTL Model-Checking.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2007

ProbDiVinE: A Parallel Qualitative LTL Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 2007

Parallel Model Checking and the FMICS-jETI Platform.

[BibT_eX]

[DOI]

Martin Leucker

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

I/O Efficient Accepting Cycle Detection.

[BibT_eX]

[DOI]

Pavel Simecek

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Distributed breadth-first search LTL model checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2006

Parallel Algorithms for Finding SCCs in Implicitly Given Graphs.

[BibT_eX]

[DOI]

Pavel Moravec

Proceedings of the Formal Methods: Applications and Technology, 2006

DiVinE - A Tool for Distributed Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Cluster-Based LTL Model Checking of Large Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

2004

From Distributed Memory Cycle Detection to Parallel LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems, 2004

2003

Distribution of Explicit-State LTL Model-Checking.

[BibT_eX]

[DOI]

Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

Parallel Breadth-First Search LTL Model-Checking.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE 2003), 2003

2001

Distributed LTL Model-Checking in SPIN.

[BibT_eX]

[DOI]