Automatyczna symboliczna weryfikacja programów i protokołów kryptograficznych w systemach rozproszonych

 

Publikacje

 

  1. A. Zbrzezny: SAT-Based Reachability Checking for Timed Automata with Diagonal Constraints. Fundamenta Informaticae 67(1-3), str. 303-322, 2005. ps.gz
  2. M. Szreter: Generalized Blocking Clauses in Unbounded Model Checking. Proc. of Int. Conf. "Constraints in Formal Verification", Tallin 2005. Ukaże się w ENTCS. ps.gz
  3. M. Szreter: Selective Search in Bounded Model Checking of Reachability Properties. Proc. of the 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05). LNCS 3707, str. 159-173, Springer-Verlag, 2005
  4. M. Kacprzak, W. Penczek: Fully Symbolic Model Checking for Alternating-Time Temporal Logic. Autonomous Agents and Multi-Agent Systems, vol. 11(1), str. 69-89, 2005
  5. A. Niewiadomski, W. Penczek, M. Szreter, M. Kacprzak: Checking Dining Cryptographers with Verics. Proc. of the Int. Workshop "Concurrency, Specification and Programming" (CS&P'05), vol. 1, str. 359-372, 2005
  6. B. Woźna, A. Lomuscio, W. Penczek: Bounded Model Checking for Knowledge and Real Time. Proc. of the 4th Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'05), str. 165-172, ACM, 2005.
  7. G. Jakubowska, W. Penczek, M. Srebrny: Verifying Security Protocols with Timestamps via Translation to Timed Automata. Proc. of the Int. Workshop "Concurrency, Specification and Programming" (CS&P'05), vol.1, str. 100-115, 2005
  8. A. Janowska, P. Janowski: Slicing of Timed Automata with Discrete Data. Proc. of the Int. Workshop "Concurrency, Specification and Programming" (CS&P'05), vol.1, str. 211-222, 2005
  9. M. Kurkowski, M. Srebrny: A Quantifier-Free First Order Knowledge Logic of Authentication. Proc. of the Int. Workshop "Concurrency, Specification and Programming" (CS&P'05), vol.1, str. 305-320, 2005
  10. M. Kurkowski: A State-Transition Model of Honest Executions of Cryptographic Protocols. Proc. of the 9th Conf. "Applications of Algebra in Logic and Computer Science" Zakopane 2005, str. 83-94, Wyd. AJD, Częstochowa 2005
  11. A. Janowska, P. Janowski: Slicing of Timed Automata with Discrete Data. Raport IPI PAN 990, luty 2006. pdf
  12. A. Janowska, P. Janowski: Slicing of Timed Automata with Discrete Data. Fundamenta Informaticae 72(1-3), str. 181-195, IOS Press, 2006. ps
  13. W. Nabiałek, P. Janowski: Towards Promela Verification using VerICS. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'06), Informatik-Berichte 206(2), str. 219-230, Humboldt University, 2006.
  14. B. Woźna and A. Zbrzezny: Bounded Model Checking for the Existential Fragment of TCTL_G and Diagonal Timed Automata. Fundamenta Informaticae 79(1-2), str. 229-256, IOS Press, 2007. pdf
  15. A. Lomuscio, B. Woźna, A. Zbrzezny: Bounded Model Checking Real-Time Multi-Agent Systems with Clock Differences: Theory and Implementation. Post-proc. of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt'06), LNAI, vol. 4428, str. 96-112, Springer-Verlag, 2007. pdf
  16. M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, M. Szreter: Comparing BDD and SAT Based Techniques for Model Checking Chaum's Dining Cryptographers Protocol. Fundamenta Informaticae 72(1-2), str. 215-234, IOS Press, 2006. ps.gz
  17. A. Niewiadomski, W. Penczek, S. Lasota, J. Kowalski: Weryfikacja UML z wykorzystaniem systemu VerICS. Mat. XIII Konferencji Systemy Czasu Rzeczywistego (SCR'06) Systemy informatyczne z ograniczeniami czasowymi, str. 79, Wyd. Komunikacji i Łączności, 2006.
  18. A. Zbrzezny, A. Półrola: SAT-Based Reachability Checking for Timed Automata with Discrete Data. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'06), Informatik-Berichte 206(2), str. 207-218, Humboldt University, 2006.
  19. M. Kurkowski, M. Srebrny: A Quantifier Free First Order Knowledge Logic of Authentication. Fundamenta Informaticae 72(1-3), str. 263-282, IOS Press, 2006.
  20. K. Grondys, M. Kurkowski, A. Sowik, I. Szczypior: Verifying Untimed Version of the WMF Protocol Using Networks of Automata. Proc. of the 10th Conf. on Applications of Algebra in Logic and Computer Science 'Zakopane 2006', str. 51-58, Wyd. AJD, Częstochowa 2006.
  21. M. Kurkowski, J. Małek, M. Orzechowski: On Some Crypto-Messages Parser. Proc. of the 10th Conf. on Applications of Algebra in Logic and Computer Science 'Zakopane 2006', str. 59-66, Wyd. AJD, Częstochowa 2006.
  22. K. Grondys, M. Kurkowski, A. Sowik, I. Szczypior: Generating and Translations of Executions of Cryptographic Protocols into Automata Networks. Proc. of the 2nd Seminar of Young Scientists 'Częstochowa 2006', str. 51-58, Wyd. AJD, Częstochowa 2006.
  23. M. Kurkowski, W. Penczek: Verifying Cryptographic Protocols Modeled by Networks of Automata. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'06), Informatik-Berichte 206(1), str. 292-303, Humboldt University, 2006.
  24. G. Jakubowska, W. Penczek: Verifying Timed Properties of Security Protocols. Raport IPI PAN 991, marzec 2006. ps.gz
  25. G. Jakubowska, W. Penczek: Modeling and Checking Timed Authentication Security Protocols. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'06), Informatik-Berichte 206(2), str. 280-291, Humboldt University, 2006. pdf
  26. W. Penczek, A. Półrola: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Springer-Verlag, 2006. Studies in Computational Intelligence 20; ISBN 3-540-32869-6
  27. B. Konikowska, W. Penczek: Model Checking for Multivalued Logic for Knowledge and Time. Proc. of the 5th Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'06), str. 169-176, ACM, 2006. pdf.gz
  28. M. Orzechowski, B. Woźna, T. Siwiak: Towards Verification of Java Programs in VerICS. Raport IPI PAN 997, grudzień 2006. ps.gz
  29. G. Jakubowska, W. Penczek: Modelling and Checking Timed Authentication of Security Protocols. Fundamenta Informaticae 79(3-4), str. 363-378, IOS Press, 2007. pdf
  30. G. Jakubowska, W. Penczek: Is Your Security Protocol on Time? Proc. of the IPM Int. Symp. on Fundamentals of Software Engineering (FSEN'07), LNCS, vol. 4767, str. 65-80, Springer-Verlag, 2007. pdf
  31. A. Janowska: Generowanie automatów czasowych dla systemów czasu rzeczywistego. Rozprawa doktorska, Uniwersytet Warszawski, wrzesień 2007. pdf
  32. A. Janowska, P. Janowski, D. Wróblewski: Translation of Intermediate Language to Timed Automata with Discrete Data. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), vol. 2, str. 309-320, Uniwersytet Warszawski, 2007. pdf
  33. A. Janowska, W. Penczek: Path Compression in Timed Automata. Fundamenta Informaticae 79(3-4), str. 379-399, IOS Press, 2007. pdf
  34. M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny: VerICS 2006 - A Model Checker for Real-Time and Multi-Agent Systems. Abstract; Proc. of the Int. Workshop on Petri Nets and Software Engineering, str. 234-235, Akademia Podlaska, 2007.
  35. M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny: VerICS 2006 - weryfikator dla systemów czasowych i wieloagentowych. Mat. Konferencji Systemy Czasu Rzeczywistego (SCR'07) Metody i zastosowania, str. 243-252, Wyd. Komunikacji i Łączności, 2007. pdf
  36. M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny: VerICS 2006 - A Model Checker for Real-Time and Multi-Agent Systems. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), vol. 2, str. 345-356, Uniwersytet Warszawski, 2007. pdf
  37. M. Kurkowski, W. Penczek: Verifying Security Protocols Modelled by Networks of Automata. Fundamenta Informaticae 79(3-4), str. 453-471, IOS Press, 2007. pdf
  38. M. Kurkowski, W. Penczek, A. Zbrzezny: SAT-Based Verification of Security Protocols via Translation to Networks of Automata. Post-proc. of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt'06), LNAI, vol. 4428, str. 146-165, Springer-Verlag, 2007. pdf
  39. A. Lomuscio, W. Penczek: Model Checking Security Protocols: A Multi-Agent System Approach. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), vol. 2, str. 400-412, Uniwersytet Warszawski, 2007. pdf
  40. A. Lomuscio, W. Penczek, B. Woźna: Bounded Model Checking for Knowledge and Real Time. Artificial Intelligence, vol. 171, str. 1011-1038, Elsevier, 2007. pdf
  41. A. Lomuscio, F. Raimondi, B. Woźna: Verification of the TESLA Protocol in MCMAS-X. Fundamenta Informaticae 79(3-4), str. 473-486, IOS Press, 2007. pdf
  42. A. Lomuscio, B. Woźna, A. Zbrzezny: Bounded Model Checking Real-Time Multi-Agent Systems with Clock Differences: Theory and Implementation. Post-proc. of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt'06), LNAI, vol. 4428, str. 96-112, Springer-Verlag, 2007. pdf
  43. A. Niewiadomski: UML Verification with VerICS. Abstract; Proc. of the Int. Workshop on Petri Nets and Software Engineering, str. 240-241, Akademia Podlaska, 2007.
  44. A. Niewiadomski, W. Penczek: UML Verification with VerICS. Ukaże się w Studia Informatica (Akademia Podlaska).
  45. W. Penczek, M. Szreter: SAT-Based Unbounded Model Checking of Timed Automata. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), vol. 2, str. 451-462, Uniwersytet Warszawski, 2007.
  46. M. Szreter: SAT-Based Model Checking of Distributed Systems. Rozprawa doktorska, IPI PAN, styczeń 2007.
  47. B. Woźna and A. Zbrzezny: Bounded Model Checking for the Existential Fragment of TCTL_G and Diagonal Timed Automata. Fundamenta Informaticae 79(1-2), str. 229-256, IOS Press, 2007. pdf
  48. A. Zbrzezny, A. Półrola: SAT-Based Reachability Checking for Timed Automata with Discrete Data. Fundamenta Informaticae 79(3-4), str. 579-593, IOS Press, 2007. pdf
  49. A. Zbrzezny, B. Woźna, M. Orzechowski, F. Raimondi: Towards Verification of Java Programs in VerICS. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), vol. 2, str. 580-593, Uniwersytet Warszawski, 2007. pdf

 

Ostatnia aktualizacja: 11.12.2007