PAT

PAT is a self-contained framework for to support composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g. partial order reduction, symmetry reduction, process counter abstraction, parallel model checking.


References in zbMATH (referenced in 36 articles )

Showing results 1 to 20 of 36.
Sorted by year (citations)

1 2 next

  1. Blondin, Michael; Esparza, Javier; Jaax, Stefan; Meyer, Philipp J.: Towards efficient verification of population protocols (2021)
  2. Esparza, Javier; Jaax, Stefan; Raskin, Mikhail; Weil-Kennedy, Chana: The complexity of verifying population protocols (2021)
  3. Liu, Yezhou; Nicolescu, Radu; Sun, Jing; Henderson, Alec: A sublinear Sudoku solution in cP systems and its formal verification (2021)
  4. Xie, Wanling; Zhu, Huibiao; Xu, Qiwen: A process calculus BigrTiMo of mobile systems and its formal semantics (2021)
  5. Liu, Yezhou; Nicolescu, Radu; Sun, Jing: Formal verification of cP systems using PAT3 and ProB (2020)
  6. Cleaveland, Rance; Roscoe, A. W.; Smolka, Scott A.: Process algebra and model checking (2018)
  7. Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)
  8. Esparza, Javier: Advances in parameterized verification of population protocols (2017)
  9. Esparza, Javier; Ganty, Pierre; Leroux, Jérôme; Majumdar, Rupak: Verification of population protocols (2017)
  10. André, Étienne: Parametric deadlock-freeness checking timed automata (2016)
  11. André, Étienne: What’s decidable about parametric timed automata? (2016)
  12. André, Étienne; Benmoussa, Mohamed Mahdi; Choppy, Christine: Formalising concurrent UML state machines using coloured Petri nets (2016)
  13. Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
  14. Al-Humaimeedy, Abeer S.; Fernández, Maribel: Enabling synchronous and asynchronous communications in CSP for SOC (2015)
  15. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P. G.: Model checking CML: tool development and industrial applications (2015) ioport
  16. André, Étienne; Liu, Yang; Sun, Jun; Dong, Jin-Song: Parameter synthesis for hierarchical concurrent real-time systems (2014)
  17. Dong, Jin Song; Liu, Yang; Sun, Jun; Zhang, Xian: Towards verification of computation orchestration (2014)
  18. Li, Xiaoru; Li, Xiaohong; Xu, Guangquan; Hu, Jing; Feng, Zhiyong: Formal analysis of fairness for optimistic multiparty contract signing protocol (2014)
  19. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  20. Si, Yuanjie; Sun, Jun; Liu, Yang; Dong, Jin Song; Pang, Jun; Zhang, Shao Jie; Yang, Xiaohu: Model checking with fairness assumptions using PAT (2014)

1 2 next


Further publications can be found at: http://pat.comp.nus.edu.sg/?page_id=2599