%0 Conference Paper %1 D'Osualdo:2012:SAS %A D'Osualdo, Emanuele %A Kochems, Jonathan %A Ong, Luke %B Proceedings of the 2nd Edition on Programming Systems, Languages and Applications Based on Actors, Agents, and Decentralized Control Abstractions %D 2012 %I ACM %K Actors Erlang StaticAnalysis %P 137--140 %R 10.1145/2414639.2414658 %T Soter: An Automatic Safety Verifier for Erlang %X This paper presents Soter, a fully-automatic program analyser and verifier for Erlang modules. The fragment of Erlang accepted by Soter includes the higher-order functional constructs and all the key features of actor concurrency, namely, dynamic and possibly unbounded spawning of processes and asynchronous message passing. Soter uses a combination of static analysis and infinite-state model checking to verify safety properties specified by the user. Given an Erlang module and a set of properties, Soter first extracts an abstract (approximate but sound) model in the form of an actor communicating system (ACS), and then checks if the properties are satisfied using a Petri net coverability checker, BFC. To our knowledge, Soter is the first fully-automatic, infinite-state model checker for a large fragment of Erlang. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties such as mutual-exclusion and boundedness of mailboxes. Though the ACS coverability problem is Expspace-complete, Soter can analyse these problems surprisingly efficiently. %@ 978-1-4503-1630-9

@inproceedings{D'Osualdo:2012:SAS, abstract = {This paper presents Soter, a fully-automatic program analyser and verifier for Erlang modules. The fragment of Erlang accepted by Soter includes the higher-order functional constructs and all the key features of actor concurrency, namely, dynamic and possibly unbounded spawning of processes and asynchronous message passing. Soter uses a combination of static analysis and infinite-state model checking to verify safety properties specified by the user. Given an Erlang module and a set of properties, Soter first extracts an abstract (approximate but sound) model in the form of an actor communicating system (ACS), and then checks if the properties are satisfied using a Petri net coverability checker, BFC. To our knowledge, Soter is the first fully-automatic, infinite-state model checker for a large fragment of Erlang. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties such as mutual-exclusion and boundedness of mailboxes. Though the ACS coverability problem is Expspace-complete, Soter can analyse these problems surprisingly efficiently.}, acmid = {2414658}, added-at = {2017-02-08T19:20:35.000+0100}, author = {D'Osualdo, Emanuele and Kochems, Jonathan and Ong, Luke}, biburl = {https://www.bibsonomy.org/bibtex/23e2798df041bb30871d1868589b62b55/gron}, booktitle = {Proceedings of the 2nd Edition on Programming Systems, Languages and Applications Based on Actors, Agents, and Decentralized Control Abstractions}, description = {Soter}, doi = {10.1145/2414639.2414658}, interhash = {4dbe357580365fb3e3b3b344c32d652e}, intrahash = {3e2798df041bb30871d1868589b62b55}, isbn = {978-1-4503-1630-9}, keywords = {Actors Erlang StaticAnalysis}, location = {Tucson, Arizona, USA}, numpages = {4}, pages = {137--140}, publisher = {ACM}, series = {AGERE! 2012}, timestamp = {2017-02-08T19:21:35.000+0100}, title = {Soter: An Automatic Safety Verifier for Erlang}, year = 2012 }