Ralf Wimmer

Ming-Yi Hu

CoRR, 2023

2022

Solving dependency quantified Boolean formulas using quantifier localization.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2022

Diagnosing Partially Observable Markov Decision Processes.

[BibT_eX]

[DOI]

Ming Hu

Leonore Winterer

Proceedings of the Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2022

The Scale4Edge RISC-V Ecosystem.

[BibT_eX]

[DOI]

Proceedings of the 2022 Design, Automation & Test in Europe Conference & Exhibition, 2022

2021

Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2021

Minimally Invasive HW/SW Co-debug Live Visualization on Architecture Level.

[BibT_eX]

[DOI]

Proceedings of the GLSVLSI '21: Great Lakes Symposium on VLSI 2021, 2021

2020

Strengthening Deterministic Policies for POMDPs.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 12th International Symposium, 2020

2019

The (D)QBF Preprocessor HQSpre - Underlying Theory and Its Implementation.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2019

Quantifier Localization for DQBF.

[BibT_eX]

[DOI]

Aile Ge-Ernst

CoRR, 2019

Correct-by-construction policies for POMDPs.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Workshop on Symbolic-Numeric methods for Reasoning about CPS and IoT, 2019

Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks.

[BibT_eX]

[DOI]

Steven Carr

Nils Jansen

Alexandru Constantin Serban

Ufuk Topcu

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019

Localizing Quantifiers for DQBF.

[BibT_eX]

[DOI]

Aile Ge-Ernst

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving.

[BibT_eX]

[DOI]

Jie-Hong Roland Jiang

Aile Ge-Ernst

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018

Finite-State Controllers of POMDPs using Parameter Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence, 2018

Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications - Extended Abstract.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Markov Automata on Discount!

[BibT_eX]

[DOI]

Yuliya Butkova

Proceedings of the Measurement, Modelling and Evaluation of Computing Systems, 2018

Abstraktions-basierte Verifikation von POMDPs im Motion-Planning-Kontext.

[BibT_eX]

[DOI]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2018

From DQBF to QBF by Dependency Elimination.

[BibT_eX]

[DOI]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2018

Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes.

[BibT_eX]

[DOI]

Proceedings of the 2018 Annual American Control Conference, 2018

Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Advanced Logic Synthesis, 2018

2017

Cost vs. time in stochastic games and Markov automata.

[BibT_eX]

[DOI]

Hassan Hatefi

Luis María Ferrer Fioriti

Formal Aspects Comput., 2017

Permissive Finite-State Controllers of POMDPs using Parameter Synthesis.

[BibT_eX]

[DOI]

CoRR, 2017

HQSpre - An Effective Preprocessor for QBF and DQBF.

[BibT_eX]

[DOI]

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

Long-Run Rewards for Markov Automata.

[BibT_eX]

[DOI]

Yuliya Butkova

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

Motion planning under partial observability using game-based abstraction.

[BibT_eX]

[DOI]

Proceedings of the 56th IEEE Annual Conference on Decision and Control, 2017

2016

Dependency Schemes for DQBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Vorwort.

[BibT_eX]

[DOI]

Proceedings of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2016

Skolem Functions for DQBF.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

Transient Reward Approximation for Continuous-Time Markov Chains.

[BibT_eX]

[DOI]

IEEE Trans. Reliab., 2015

High-level Counterexamples for Probabilistic Automata

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Abstraction-Based Computation of Reward Measures for Markov Automata.

[BibT_eX]

[DOI]

Luis María Ferrer Fioriti

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

Modeling Unknown Values in Test and Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems, 2015

Preprocessing for DQBF.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Towards Verification of Artificial Neural Networks.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2015

Counterexamples for Expected Rewards.

[BibT_eX]

[DOI]

Proceedings of the FM 2015: Formal Methods, 2015

Solving DQBF through quantifier elimination.

[BibT_eX]

[DOI]

Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, 2015

2014

Minimal counterexamples for linear-time probabilistic verification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2014

Symbolic counterexample generation for large discrete-time Markov chains.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata.

[BibT_eX]

[DOI]

Luis María Ferrer Fioriti

Proceedings of the Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, 2014

Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Executable Software Models, 2014

Accelerating Parametric Probabilistic Verification.

[BibT_eX]

[DOI]

Proceedings of the Quantitative Evaluation of Systems - 11th International Conference, 2014

Maybe or Maybe Not: Contributions to Stochastic Verification.

[BibT_eX]

Erika Ábrahám

Proceedings of the Aspekte der Technischen Informatik, 2014

Fast Debugging of PRISM Models.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Equivalence Checking for Partial Implementations Revisited.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2013

Stochastic Bounded Model Checking: Bounded Rewards and Compositionality.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2013

Equivalence checking of partial designs using dependency quantified Boolean formulae.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE 31st International Conference on Computer Design, 2013

2012

Transient Reward Approximation for Grids, Crowds, and Viruses

[BibT_eX]

[DOI]

CoRR, 2012

The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains

[BibT_eX]

[DOI]

CoRR, 2012

Minimal Critical Subsystems for Discrete-Time Markov Models.

[BibT_eX]

[DOI]

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

Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2012

Symbolic Counterexample Generation for Discrete-Time Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012

The COMICS Tool - Computing Minimal Counterexamples for DTMCs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2012

2011

Symbolische Methoden für die probabilistische Verifikation: Zustandsraumreduktion und Gegenbeispiele.

[BibT_eX]

[DOI]

PhD thesis, 2011

Reachability analysis for incomplete networks of Markov decision processes.

[BibT_eX]

[DOI]

Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011

SMT-based Counterexample Generation for Markov Chains.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Symbolische Methoden für die probabilistische Verifikation: Zustandsraumreduktion und Gegenbeispiele.

[BibT_eX]

[DOI]

Proceedings of the Ausgezeichnete Informatikdissertationen 2011, 2011

Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2011

Hierarchical Counterexamples for Discrete-Time Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2011

Bounded Fairness for Probabilistic Distributed Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Application of Concurrency to System Design, 2011

2010

Symbolic partition refinement with automatic balancing of time and space.

[BibT_eX]

[DOI]

Salem Derisavi

Perform. Evaluation, 2010

Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems.

[BibT_eX]

[DOI]

Proceedings of the QEST 2010, 2010

DTMC Model Checking by SCC Reduction.

[BibT_eX]

[DOI]

Proceedings of the QEST 2010, 2010

Correctness Issues of Symbolic Bisimulation Computation for Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Measurement, 2010

Exploiting Different Strategies for the Parallelization of an SMT Solver.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2010

A Model Checker for AADL.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Compositional Dependability Evaluation for STATEMATE.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2009

Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2009

Dependability Engineering of Silent Self-stabilizing Systems.

[BibT_eX]

[DOI]

Proceedings of the Stabilization, 2009

Picoso - A Parallel Interval Constraint Solver.

[BibT_eX]

Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 2009

2008

Symbolic Partition Refinement with Dynamic Balancing of Time and Space.

[BibT_eX]

[DOI]

Salem Derisavi

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

The Demand for Reliability in Probabilistic Verification.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2008

Propositional approximations for bounded model checking of partial circuit designs.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Computer Design, 2008

Probabilistic Model Checking and Reliability of Results.

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS 2008), 2008

2007

Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation.

[BibT_eX]

Marc Herbstritt

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2007

Optimization techniques for BDD-based bisimulation computation.

[BibT_eX]

[DOI]

Marc Herbstritt

Proceedings of the 17th ACM Great Lakes Symposium on VLSI 2007, 2007

2006

Compositional Performability Evaluation for STATEMATE.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006

Minimization of Large State Spaces using Symbolic Branching Bisimulation.

[BibT_eX]

[DOI]

Marc Herbstritt