@inproceedings{cassez-lpar-2015,
  author    = {Franck Cassez and
               Frowin Ziegler},
                editor    = {Martin Davis and
               Ansgar Fehnker and
               Annabelle McIver and
               Andrei Voronkov},
  title     = {Verification of Concurrent Programs Using Trace Abstraction Refinement},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,
               2015, Proceedings},
  pages     = {233--248},
  year      = {2015},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  publisher = {Springer},
  year      = {2015},
  url       = {http://dx.doi.org/10.1007/978-3-662-48899-7_17},
  mywebpage = {soft-verif},
  category = {soft-verif},
  isbn      = {978-3-662-48898-0},
  doi       = {10.1007/978-3-662-48899-7_17},
  show = {},
  note = {LPAR Best paper award},
  urlpaper = {papers/lpar-2015.pdf},
    urlslides = {papers/slides-lpar-2015.pdf},
  abstract = {Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.},
  Type = {B - International Conferences},
}

{"_id":"mFuHL9ACDFim6eczS","bibbaseid":"cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015","author_short":["Cassez, F.","Ziegler, F."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Frowin"],"propositions":[],"lastnames":["Ziegler"],"suffixes":[]}],"editor":[{"firstnames":["Martin"],"propositions":[],"lastnames":["Davis"],"suffixes":[]},{"firstnames":["Ansgar"],"propositions":[],"lastnames":["Fehnker"],"suffixes":[]},{"firstnames":["Annabelle"],"propositions":[],"lastnames":["McIver"],"suffixes":[]},{"firstnames":["Andrei"],"propositions":[],"lastnames":["Voronkov"],"suffixes":[]}],"title":"Verification of Concurrent Programs Using Trace Abstraction Refinement","booktitle":"Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings","pages":"233–248","year":"2015","series":"Lecture Notes in Computer Science","volume":"9450","publisher":"Springer","url":"http://dx.doi.org/10.1007/978-3-662-48899-7_17","mywebpage":"soft-verif","category":"soft-verif","isbn":"978-3-662-48898-0","doi":"10.1007/978-3-662-48899-7_17","show":"","note":"LPAR Best paper award","urlpaper":"papers/lpar-2015.pdf","urlslides":"papers/slides-lpar-2015.pdf","abstract":"Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.","bibtex":"@inproceedings{cassez-lpar-2015,\n author = {Franck Cassez and\n Frowin Ziegler},\n editor = {Martin Davis and\n Ansgar Fehnker and\n Annabelle McIver and\n Andrei Voronkov},\n title = {Verification of Concurrent Programs Using Trace Abstraction Refinement},\n booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th\n International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,\n 2015, Proceedings},\n pages = {233--248},\n year = {2015},\n series = {Lecture Notes in Computer Science},\n volume = {9450},\n publisher = {Springer},\n year = {2015},\n url = {http://dx.doi.org/10.1007/978-3-662-48899-7_17},\n mywebpage = {soft-verif},\n category = {soft-verif},\n isbn = {978-3-662-48898-0},\n doi = {10.1007/978-3-662-48899-7_17},\n show = {},\n note = {LPAR Best paper award},\n urlpaper = {papers/lpar-2015.pdf},\n urlslides = {papers/slides-lpar-2015.pdf},\n abstract = {Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.},\n Type = {B - International Conferences},\n}\n\n","author_short":["Cassez, F.","Ziegler, F."],"editor_short":["Davis, M.","Fehnker, A.","McIver, A.","Voronkov, A."],"key":"cassez-lpar-2015","id":"cassez-lpar-2015","bibbaseid":"cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/lpar-2015.pdf","Slides":"http://science.mq.edu.au/~fcassez/bib/papers/slides-lpar-2015.pdf"},"metadata":{"authorlinks":{}},"downloads":1},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F"],"keywords":[],"search_terms":["verification","concurrent","programs","using","trace","abstraction","refinement","cassez","ziegler"],"title":"Verification of Concurrent Programs Using Trace Abstraction Refinement","year":2015,"downloads":1}