TyPiCal: type-based static analyzer for the Pi-Calculus. TyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides the following program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, information flow analysis, and termination analysis. The former two analyses aim to statically analyze whether each communication succeeds or not. The lock-freedom analysis can answer, e.g., the following questions about the behavior of concurrent/distributed programs: Does the server eventually accept every request from a client? Does the server eventually send a reply to every request? Can a process eventually acquire a lock? Does a process that has acquired a lock eventually release the lock? Useless-code elimination (UCE) optimizes a pi-calculus process by removing sub-processes that do not affect the observable behavior of the process. The result of UCE is barbed congruent to the original process, but often simpler than the original process, so that it is more efficient, and easier to verify (with other tools such as model checkers). Information flow analyzer checks whether a process leaks information about secret data to the environment. You can try web interface for TyPiCal’s deadlock-freedom analysis here.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Kobayashi, Naoki; Laneve, Cosimo: Deadlock analysis of unbounded process networks (2017)
- Stadtmüller, Kai; Sulzmann, Martin; Thiemann, Peter: Static trace-based deadlock analysis for synchronous mini-go (2016)
- Giachino, Elena; Laneve, Cosimo: Deadlock detection in linear recursive programs (2014)
- Lapadula, A.; Pugliese, R.; Tiezzi, F.: A WSDL-based type system for asynchronous WS-BPEL processes (2011)
- Demangeon, Romain; Hirschkoff, Daniel; Sangiorgi, Davide: Mobile processes and termination (2009)
- Acciai, Lucia; Boreale, Michele: Responsiveness in process calculi (2008)
- Kobayashi, Naoki: Type-based information flow analysis for the (\pi)-calculus (2005)
- Han, Te Sun; Kobayashi, Kingo: Maximal rectangular subsets contained in the set of partially jointly typical sequences for dependent random variables (1985)