dr Andrzej Zbrzezny

Publikacje

Rok 2009

• B. Woźna, A. Zbrzezny
  SAT-based searching for k-quasi-optimal runs in weighted timed automata
  Materiały konferencji: Concurrency, Specification and Programming (CS&P'2009)
  Kraków-Przegorzały, 28-30 wrzesień 2009. W druku.

• A. Rataj, B. Woźna, A. Zbrzezny
  A translator of Java programs to TADDs
  Fundamenta Informaticae 93(1-3), str. 305-324, 2009.

• B. Woźna, A. Zbrzezny
  Verification of Java programs using networks of finite automata with discrete data
  Scientific Issues: Mathematica II, str. 89-99. Catholic University in Ruzomberok, 2009.

• Wojciech Penczek, Agata Półrola, Andrzej Zbrzezny
  SAT-Based (Parametric) Reachability for Distributed Time Petri Nets
  Materiały konferencji: International Workshop on Petri Nets and Software Engineering (PNSE'09)
  str.133-156, University of Hamburg, Department of Informatics. Paryż, Francja, Czerwiec 22-23, 2009.

• Kacprzak M., Nabiałek W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Woźna B., Zbrzezny A.
  VerICS 2008 - a Model Checker for Time Petri Nets and High-Level Languages
  Materiały konferencji: International Workshop on Petri Nets and Software Engineering (PNSE'09)
  str.119-132, University of Hamburg, Department of Informatics. Paryż, Francja, Czerwiec 22-23, 2009.

Rok 2008

• A. Zbrzezny
  Improving the Translation from ECTL to SAT
  Fundamenta Informaticae, 85(1-4), str. 513-531, 2008.

• A. Zbrzezny, B. Woźna
  Towards verification of Java programs in Verics
  Fundamenta Informaticae, 85(1-4), str. 532-548, 2008.

• M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny
  VerICS 2007 - a Model Checker for Knowledge and Real-Time
  Fundamenta Informaticae, 85(1-4), str. 313-328, 2008.

• A. Zbrzezny
  A Boolean Encoding of Arithmetic Operations
  Materiały konferencji: Concurrency, Specification and Programming (CS&P'2008), volume 3, str. 536-547
  Groß Väter See, September 2008.

• A. Rataj, B. Woźna, A. Zbrzezny
  A translator of Java programs to TADDs
  Materiały konferencji: Concurrency, Specification and Programming (CS&P'2008), volume 3, str. 524-535
  Groß Väter See, September 2008.

• Kacprzak M., Nabiałek W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Woźna B., Zbrzezny A
  VerICS 2008 - a Model Checker for High-Level Languages
  Artificial Intelligence Studies, 2008, tom. 5 (28)/2008, str.131-140.
  

• B. Woźna, A. Zbrzezny
  A SAT-based technique to analyse networks of finite automata
  Scientific Issues: Mathematica II,
  str. 89-100. Catholic University in Ruzomberok, 2008.

Rok 2007

• A. Zbrzezny
  Improving the Translation from ECTL to SAT (pdf).
  In Proceedings of CS&P'2007 Workshop, volume 2, str. 568-579, Łagów, September 2007.

• A. Zbrzezny, A. Półrola.
  SAT-Based Reachability Checking for Timed Automata with Discrete Data
  Fundamenta Informaticae 79(3-4), str. 579-593, 2007.

• B. Woźna, A. Zbrzezny.
  Bounded Model Checking for the Existential Fragment of TCTL_G and Diagonal Timed Automata.
  Fundamenta Informaticae 79(1-2), str. 229-256, 2007.

• A. Lomuscio, B. Woźna, A. Zbrzezny.
  Bounded model checking real-time multi-agent systems with clock differences: theory and implementation.
  In Post-Proceedings of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt'06), LNAI/LNCS, volume 4428, str. 96-112. Springer-Verlag, 2007.

• M. Kurkowski, W. Penczek, A. Zbrzezny.
  SAT-based Verification of Security Protocols via Translation to Networks of Automata.
  In Post-Proceedings of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt'06), LNAI/LNCS, volume 4428, str. 96-112. Springer-Verlag, 2007.

• A. Zbrzezny.
  A Boolean Encoding of Arithmetic Operations. (gzipped ps).
  Report ICS PAS, 999, January 2007.

Rok 2006

• A. Zbrzezny, A. Półrola.
  SAT-Based Reachability Checking for Timed Automata with Discrete Data
  In Proceedings of CS&P'2006 Workshop, volume 2, str. 207-218, Wandlitz 2006.

Rok 2005

• A. Zbrzezny.
  SAT-based Reachability Checking for Timed Automata with Diagonal Constraints.
  Fundamenta Informaticae 67(1-3), str. 303-322, 2005.

• B. Woźna, A. Zbrzezny.
  Bounded Model Checking for the Existential Fragment of TCTL and Diagonal Timed Automata.
  In Proceedings of the CS&P'2005 Workshop, volume 2, str. 586-597, Ruciane Nida 2005

Rok 2004

• B. Woźna, A. Zbrzezny.
  Checking ACTL* Properties of Discrete Timed Automata via Bounded Model Checking.
  In Proceedings of FORMATS'2003, volume 2791 of LNCS, str. 18 - 33, Springer-Verlag, 2004.

• B. Woźna, A. Zbrzezny.
  Checking ACTL* properties of Discrete Timed Automata via Bounded Model Checking. (Revised version of the paper published in Proceedings of the 1st International Workshop on Formal Analysis and Modeling of Timed Systems).
  Technical Report TR-04-04, Department of Computer Science, King's College London, 2004.

• A. Zbrzezny.
  Improvements in SAT-based Reachability Analysis for Timed Automata.
  Fundamenta Informaticae 60(1-4), str. 417-434, 2004.

• W. Penczek, A. Półrola, B. Woźna, A. Zbrzezny.
  Bounded Model Checking for Reachability Testing in Time Petri Nets.
  In Proceedings of CS&P'2004 Workshop, volume 1, str. 124-135, Caputh 2004

• A. Zbrzezny.
  A New Discretization for Timed Automata.
  In Proceedings of CS&P'2004 Workshop, volume 1, str. 178-189, Caputh 2004

Rok 2003

• P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny.
  VERICS: A Tool for Verifying Timed Automata and Estelle Specifications.
  In Proc. of the 9th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, str. 278-283, Springer-Verlag, 2003.

• B. Woźna, A. Zbrzezny.
  Reaching the limits for Bounded Model Checking.
  Report ICS PAS, 958, May 2003.

• B. Woźna, A. Zbrzezny, W. Penczek.
  Checking Reachability Properties for Timed Automata via SAT.
  Fundamenta Informaticae 55(2), str. 223-241, 2003.

• P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny.
  VerICS: weryfikator dla automatów czasowych i specyfikacji zapisanych w języku Estelle (VerICS: A Tool for Verifying Timed Automata and Estelle Specifications).
  In Proc. of SCR'03, 2003.

• A. Zbrzezny.
  Improvements in SAT-based Reachability Analysis for Timed Automata.
  In Proceedings of the CS&P'2003 Workshop, volume 2, str. 606-619, Warsaw University, 2003.

Rok 2002

• W. Penczek, B. Woźna, A. Zbrzezny.
  Branching Time Bounded Model Checking for Elementary Net Systems.
  Report ICS PAS, 940, January 2002.

• W. Penczek, B. Woźna, A. Zbrzezny.
  Bounded Model Checking for the Universal Fragment of CTL.
  Fundamenta Informaticae, volume 51(1-2), 2002 str. 135-156.

• W. Penczek, B. Woźna, A. Zbrzezny.
  Towards Bounded Model Checking for the Universal Fragment of TCTL.
  In Proceedings of FTRTFT'02, volume 2469 of LNCS, Springer-Verlag, 2002.

• B. Woźna, W. Penczek, A. Zbrzezny.
  Reachability for Timed Systems based on SAT-Solvers.
  In Proceedings of CS&P'2002 Workshop, volume 2, Berlin 2002

• W. Penczek, B. Woźna, A. Zbrzezny.
  SAT-Based Bounded Model Checking for the Universal Fragment of TCTL.
  Report ICS PAS, 947, September 2002

• B. Woźna, W. Penczek, A. Zbrzezny.
  Checking Reachability Properties for Timed Automata via SAT.
  Report ICS PAS, 949, October 2002

Lata 1988-2001

• A. Zbrzezny.
  The Gentzen type axiomatization of some three-valued propositional logic.
  Bulletin of the Section of Logic 17 (1988), str. 70-74.

• A. Zbrzezny.
  The sequent axiomatization of some three-valued propositional logic.
  Proceedings of the V Universal Algebra Symposium, Universal and Applied Algebra, Turawa 1988, World Scientific, Singapore, New Jersey, London Hong Kong (1989) str. 378-388

• A. Zbrzezny.
  The Hilbert type axiomatization of some three-valued propositional logic.
  Zeitschrift fur Marhematische Logik und Grundlagen der Mathematik 36 (1990), str. 415-421.

• A. Zbrzezny.
  On a three-valued internal logic of programs.
  Prace Naukowe Wyższej Szkoły Pedagogicznej w Częstochowie, Matematyka II (1996-1998) str. 105-121.

• A. Zbrzezny.
  Natural deduction system for some three-valued propositional logic.
  Prace Naukowe Wyższej Szkoły Pedagogicznej w Częstochowie, Matematyka VI (1999) str. 148-152.

• A. Zbrzezny.
  A note on some class of locally Boolean Algebras.
  Prace Naukowe Wyższej Szkoły Pedagogicznej w Częstochowie, Matematyka VIII (2000-2001) str. 107-112.

Wykształcenie

1976-1981 - studia na kierunku Informatyka, Uniwersytet Jagielloński
1981 - magister informatyki, Instytut Informatyki, Uniwersytet Jagielloński
1991 - doktor nauk humanistycznych w zakresie filozofii; specjalność: logika, Wydział Nauk Społecznych, Uniwersytet Wrocławski

Przebieg pracy zawodowej

1981-1991 - asystent w Instytucie Matematyki Wyższej Szkoły Pedagogicznej w Częstochowie
od 1991 adiunkt w Instytucie Matematyki Wyższej Szkoły Pedagogicznej w Częstochowie

Zainteresowania naukowe

• Logika
  • Logiki Wielowartościowe
  • Logiki Tolerujące Sprzeczności (Paraconsistent logics)
  • Logiki Temporalne
• Teoria i praktyka programowania
  • Programowanie w języku C++
  • Programowanie w języku Java™
  • Dowodzenie poprawności programów
• Symboliczna Weryfikacja Modelowa
• Automaty Czasowe

Zainteresowania prywatne

• Szachy

• Giełda

• Tenis ziemny

ADRES SŁUŻBOWY
ul. Armii Krajowej 13/15
42-200 Częstochowa

Materiały dla studentów

e-mail służbowy: a.zbrzezny@ajd.czest.pl
e-mail dla studentów: andrzej.zbrzezny@gmail.com