@InProceedings{sofsem12, author = {P. Jaru\v{s}ek and R. Pel\'anek}, title = {Modeling and Predicting Students Problem Solving Times}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proc. of International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2012)}, OPTpages = {}, year = {2012}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, series = {LNCS}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, note = {To appear.}, OPTannote = {} } @InProceedings{edm11, author = {P. Jaru\v{s}ek and R. Pel\'anek}, title = {Problem Response Theory and its Application for Tutoring}, booktitle = {Educational Data Mining}, pages = {374-375}, year = {2012}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {ISBN 978-90-386-2537-9}, OPTannote = {} } @InProceedings{transport-flairs, author = {P. Jaru\v{s}ek and R. Pel\'anek}, title = {What Determines Difficulty of Transport Puzzles?}, booktitle = {Proc. of Florida Artificial Intelligence Research Society Conference (FLAIRS 2011)}, pages = {428-433}, year = {2011}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTpublisher = {}, OPTnote = {}, } @InProceedings{sudoku-flairs, author = {R. Pel\'anek}, title = {Difficulty rating of Sudoku Puzzles by a Computational Model}, booktitle = {Proc. of Florida Artificial Intelligence Research Society Conference (FLAIRS 2011)}, pages = {434-439}, year = {2011}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTpublisher = {}, OPTnote = {}, } @TechReport{sudoku-tr, author = {R. Pel\'anek}, title = {Human Problem Solving: Sudoku Case Study}, institution = {Masaryk University Brno}, year = {2011}, number = {FIMU-RS-2011-01}, } @TechReport{sokoban-tr, author = {P. Jaru\v{s}ek and R. Pel\'anek}, title = {Human Problem Solving: Sokoban Case Study}, institution = {Masaryk University Brno}, year = {2010}, number = {FIMU-RS-2010-01}, } @InProceedings{sokoban-stairs, author = {P. Jaru\v{s}ek and R. Pel{\'a}nek}, title = {Difficulty Rating of Sokoban Puzzle}, booktitle = {Proc. of the Fifth Starting AI Researchers' Symposium (STAIRS 2010)}, year = {2010}, pages = {140-150}, publisher = {IOS Press}, } @inproceedings{emma-spin, author = {R. Pel{\'a}nek and V. Roseck{\'y}}, title = {EMMA: Explicit Model Checking Manager (Tool Presentation)}, booktitle = {Proc. of Model Checking Software (SPIN'09)}, year = {2009}, pages = {169-173}, publisher = {Springer}, series = {LNCS}, volume = {5578}, } @article{sttt08-properties, author = {R. Pel{\'a}nek}, title = {Properties of state spaces and their applications}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {10}, number = {5}, year = {2008}, pages = {443-454}, } @InProceedings{beem, author = {R. Pel\'anek}, title = {BEEM: Benchmarks for Explicit Model Checkers}, booktitle = {Proc. of SPIN Workshop}, pages = {263-267}, year = {2007}, volume = {4595}, series = {LNCS}, publisher = {Springer}, } @InProceedings{fmics08-review, author = {R. Pel\'anek}, title = {Fighting State Space Explosion: Review and Evaluation}, booktitle = {Proc. of Formal Methods for Industrial Critical Systems (FMICS'08)}, OPTpages = {}, year = {2008}, OPTvolume = {}, OPTseries = {LNCS}, OPTpublisher = {Springer}, note = {To appear.} } @article{bug-hunt, author = {R. Pel\'anek and V. Roseck\'y and P. Moravec}, title = {Complementarity of Error Detection Techniques}, journal = {ENTCS}, volume = {220}, number = {2}, year = {2008}, pages = {51-65}, } @InProceedings{classifications, author = {R. Pel\'anek}, title = {Model Classifications and Automated Verification}, booktitle = {Proc. of Formal Methods for Industrial Critical Systems (FMICS'07)}, pages = {149-163}, year = {2008}, volume = {4916}, series = {LNCS}, publisher = {Springer}, } @Article{lmcs-underapproximation, author = {C. Pasareanu and R. Pel\'anek and W. Visser}, title = {Predicate Abstraction with Under-Approximation Refinement}, journal = {Logical Methods in Computer Science}, year = {2007}, volume = {3}, number = {1}, } @PhdThesis{phd-thesis, author = {R. Pel\'anek}, title = {Reduction and Abstraction Techniques for Model Checking}, school = {Faculty of Informatics, Masaryk University, Brno}, year = {2006}, } @article{BBLP-STTT05, author = {G. Behrmann and P. Bouyer and K. G. Larsen and R. Pel{\'a}nek}, journal = {International Journal on Software Tools for Technology Transfer}, title = {Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata}, volume = {8}, number = {3}, year = {2006}, issn = {1433-2779}, pages = {204--215}, publisher = {Springer}, } @InProceedings{fsttcs05sampled, author = {P. Kr\v{c}\'al and R. Pel\'anek}, title = {On Sampled Semantics of Timed Systems}, booktitle = {Proc. of Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05)}, pages = {310-321}, year = {2005}, volume = {3821}, series = {LNCS}, publisher = {Springer}, } @InProceedings{memics05, author = {R. Pel\'anek}, title = {Evaluation of On-the-fly State Space Reductions}, booktitle = {Proc. of Mathematical and Engineering Methods in Computer Science (MEMICS'05)}, pages = {121-127}, year = {2005}, } @InProceedings{ase05testing, author = {C. Pasareanu and R. Pel\'anek and W. Visser}, title = {Test Input Generation for Red Black Trees using Abstraction}, booktitle = {Proc. of Automated Software Engineering (ASE'05)}, year = {2005}, pages = {414-417}, publisher = {ACM} } @InProceedings{random-walk, author = {R. Pel\'{a}nek and T. Han\v{z}l and I. \v{C}ern\'{a} and L. Brim}, title = {Enhancing Random Walk State Space Exploration}, booktitle = {Proc. of Formal Methods for Industrial Critical Systems (FMICS'05)}, year = {2005}, pages = {98--105}, OPTlocation = {Lisbon, Portugal}, OPTisbn = {1-59593-148-1}, publisher = {ACM Press}, } @InProceedings{ciaa05, author = {R. Pel\'anek and J. Strej\v{c}ek}, title = {Deeper Connections between {LTL} and Alternating Automata}, booktitle = {Proc. of Conference on Implementation and Application of Automata (CIAA 2005)}, pages = {238-245}, year = {2005}, volume = {3845}, series = {LNCS}, publisher = {Springer}, } @InProceedings{cav05, author = {C. Pasareanu and R. Pel\'anek and W. Visser}, title = {Concrete Model Checking with Abstract Matching and Refinement}, booktitle = {Proc. of Computer Aided Verification (CAV 2005)}, pages = {52-66}, year = {2005}, volume = {3576}, series = {LNCS}, publisher = {Springer}, } @InProceedings{lu-bounds, author = {G. Behrmann and P. Bouyer and K. G. Larsen and R. Pel\'anek }, title = {Lower and Upper Bounds in Zone Based Abstractions of Timed Automata}, booktitle = {Proc. of Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)}, pages = {312-326}, year = {2004}, volume = {2988}, series = {LNCS}, publisher = {Springer} } @InProceedings{to-store, author = {G. Behrmann and K. G. Larsen and R. Pel\'anek}, title = {To Store or Not To Store}, booktitle = {Proc. of Computer Aided Verification (CAV 2003)}, year = {2003}, volume = {2725}, series = {LNCS}, publisher= {Springer}, } @InProceedings{properties, author = {R. Pel\'anek}, title = {Typical Structural Properties of State Spaces}, booktitle = {Proc. of SPIN Workshop}, pages = {5-22}, year = {2004}, volume = {2989}, series = {LNCS}, publisher= {Springer}, } @InProceedings{BCKP-FSTTCS01, author = {L. Brim and I. \v{C}ern\'{a} and P. Kr\v{c}\'{a}l and R. Pel\'{a}nek}, title = {Distributed {LTL} Model Checking Based on Negative Cycle Detection}, booktitle = {Proc. of Foundations of Software Technology and Theoretical Computer Science (FST TCS 2001)}, pages = {96-107}, year = {2001}, volume = {2245}, series = {LNCS}, publisher = {Springer} } @InProceedings{BCKP-SOFSEM01, author = {L. Brim and I. \v{C}ern\'{a} and P. Kr\v{c}\'{a}l and R. Pel\'{a}nek}, title = {How to Employ Reverse Search in Distributed Single-Source Shortest Paths}, booktitle = {Proc. SOFSEM'01}, pages = {191-200}, year = {2001}, volume = {2234}, series = {LNCS}, publisher = {Springer} } @InProceedings{distributed-set-based-spin, author = {I. {\v{C}}ern\'a and R. Pel\'anek}, title = {Distributed Explicit Fair Cycle Detection}, booktitle = {Proc. {SPIN} workshop}, year = {2003}, volume = {2648}, series = {LNCS}, pages = {49-73}, publisher= {Springer}, } @InProceedings{hierarchy-mfcs, author = {I. {\v{C}}ern\'a and R. Pel\'anek}, title = {Relating Hierarchy of Temporal Properties to Model Checking}, booktitle = {Proc. of Mathematical Foundations of Computer Science (MFCS 2003)}, year = {2003}, volume = {2747}, series = {LNCS}, pages = {318-327}, publisher= {Springer}, } @TechReport{reductions-tech-rep, author = {R. Pel\'anek}, title = {On-the-fly State Space Reductions}, institution = {Masaryk University Brno}, year = {2005}, number = {FIMU-RS-2005-03}, } @TechReport{ltl-aa, author = {R. Pel\'anek and J. Strej\v{c}ek}, title = {Deeper Connections between LTL and Alternating Automata}, institution = {Masaryk University Brno}, year = {2004}, number = {FIMU-RS-2004-08}, } @TechReport{hierarchy-tech-rep, author = {I. {\v{C}}ern\'a and R. Pel\'anek}, title = {Relating Hierarchy of Linear Temporal Properties to Model Checking}, institution = {Faculty of Informatics, Masaryk University Brno}, year = {2003}, number = {FIMU-RS-2003-03}, month = {April}, } @TechReport{spin03-tech-rep, author = {I. {\v{C}}ern\'a and R. Pel\'anek}, title = {Distributed Explicit Fair Cycle Detection: Set Based Approach}, institution = {Faculty of Informatics, Masaryk University Brno}, year = {2002}, number = {FIMU-RS-2002-09}, month = {December}, } @TechReport{reverse-search-tech-rep, author = {L. Brim and P. Kr\v{c}\'al and I. {\v{C}}ern\'a and R. Pel\'anek}, title = {How to Employ Reverse Search in Distributed Single Source Shortest Paths}, institution = {Faculty of Informatics, Masaryk University Brno}, year = {2001}, number = {FIMU-RS-2001-09}, month = {November}, } @TechReport{negative-cycles-tech-rep, author = {I. {\v{C}}ern\'a and R. Pel\'anek}, title = {Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths}, institution = {Faculty of Informatics, Masaryk University Brno}, year = {2001}, number = {FIMU-RS-2001-01}, month = {May}, } @InProceedings{esslli-hierarchy, author = {R. Pel\'anek}, title = {LTL Hierarchies and Model Checking}, booktitle = {ESSLLI Student Session}, year = {2003}, } @MastersThesis{pelanek-thesis, author = {R. Pel\'{a}nek}, title = {{LTL} Model Checking}, school = {Faculty of Informatics, Masaryk University, Brno}, year = {2003}, } @InProceedings{issta06, author = {C. Pasareanu and R. Pel\'anek and W. Visser}, title = {Test Input Generation for Java Containers using State Matching.}, booktitle = {Proc. of International Symposium on International Symposium on Software Testing and Analysis (ISSTA'06)}, pages = {37--48}, year = {2006}, publisher = {ACM}, } @TechReport{beem-tr, author = {R. Pel\'anek}, title = {Web Portal for Benchmarking Explicit Model Checkers}, institution = {Masaryk University Brno}, year = {2006}, number = {FIMU-RS-2006-03}, } @TechReport{estimation-tr, author = {R. Pel\'anek and P. \v{S}ime\v{c}ek}, title = {Estimating State Space Parameters}, institution = {Masaryk University Brno}, year = {2008}, number = {FIMU-RS-2008-01}, } @TechReport{caching-comprossion-tr, author = {R. Pel\'anek and V. Roseck\'{y} and J. \v{S}ed\v{e}nka}, title = {Evaluation of State Caching and State Compression Techniques}, institution = {Masaryk University Brno}, year = {2008}, number = {FIMU-RS-2008-02}, } @TechReport{emma-tr, author = {R. Pel\'anek and V. Roseck\'{y}}, title = {Verification Manager: Automating the Verification Process}, institution = {Masaryk University Brno}, year = {2009}, number = {FIMU-RS-2009-02}, }