Dalal Alrajeh, Antoine Cailliau, and Axel van Lamsweerde. Adapting requirements models to varying environments. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE ?20, page 50-61, New York, NY, USA, 2020. Association for Computing Machinery
Dalal Alrajeh and Robert Craven. Automated error-detection and repair for compositional software specifications. In Dimitra Giannakopoulou and Gwen Salaön, editors, Software Engineering and Formal Methods, pages 111-127, Cham, 2014. Springer International Publishing
R. Alur and S. La Torre. Deterministic generators and games for LTL fragments. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pages 291-300, June 2001
Rajeev Alur, Salar Moarref, and Ufuk Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 26-33, 2013
Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. IFAC Proceedings Volumes, 31(18):447-452, 1998. 5th IFAC Conference on System Structure and Control 1998 (SSC?98), Nantes, France
Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. Automata-based model counting for string constraints. In Computer Aided Verification-27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 255-272, 2015
Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol., 20(4):14:1-14:64, 2011
Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa?ar. Synthesis of reactive(1) designs. J. Comput. Syst. Sci., 78(3):911-938, 2012
Davide G Cavezza and Dalal Alrajeh. Interpolation-based GR(1) assumptions refinement. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 281-297. Springer, 2017
Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. Environment assumptions for synthesis. In Franck van Breugel and Marsha Chechik, editors, CONCUR 2008-Concurrency Theory, pages 147-161, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg
George Chatzieleftheriou, Borzoo Bonakdarpour, Panagiotis Katsaros, and Scott A. Smolka. Abstract model repair. Log. Methods Comput. Sci., 11(3), 2015
A. Cimatti, M. Roveri, V. Schuppan, and A. Tchaltsev. Diagnostic information for realizability. In Proc. of the 9th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation, pages 52-67, 2008
Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT Press, 2001
Renzo Degiovanni, Dalal Alrajeh, Nazareno Aguirre, and Sebastian Uchitel. Automated goal operationalisation based on interpolation and sat solving. In ICSE, pages 129-139, 2014
Renzo Degiovanni, Pablo F. Castro, Marcelo Arroyo, Marcelo Ruiz, Nazareno Aguirre, and Marcelo F. Frias. Goal-conflict likelihood assessment based on model counting. In Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, pages 1125-1135, 2018
Renzo Degiovanni, Facundo Molina, German Regis, and Nazareno Aguirre. A genetic algorithm for goal-conflict identification. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, pages 520-531, 2018
Renzo Degiovanni, Nicolas Ricci, Dalal Alrajeh, Pablo F. Castro, and Nazareno Aguirre. Goal-conflict detection based on temporal satisfiability checking. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pages 507-518, 2016
Nicolas D?Ippolito, Victor A. Braberman, Nir Piterman, and Sebastian Uchitel. Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol., 22(1):9, 2013
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In ICSE, pages 411-420, 1999
E. Allen Emerson and Edmund M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program., 2(3):241-266, 1982
Bernd Finkbeiner and Hazem Torfah. Counting models of linear-Time temporal logic. In Adrian Horia Dediu, Carlos Martin-Vide, Jose Luis Sierra-Rodriguez, and Bianca Truthe, editors, Language and Automata Theory and Applications-8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, volume 8370 of Lecture Notes in Computer Science, pages 360-371. Springer, 2014
Gordon Fraser, Franz Wotawa, and Paul Ammann. Testing with model checkers: A survey. Softw. Test., Verif. Reliab., 19(3):215-261, 2009
D. Goldberg. Genetic Algorithms in Search, Optimization and Machine Learning. Addison-Wesley, 1989
Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island., pages 203-208, 1997
Robert Könighofer, Georg Hofferek, and Roderick Bloem. Debugging formal specifications: A practical approach using model-based diagnosis and counterstrategies. Int. J. Softw. Tools Technol. Transf., 15(5-6):563-583, 2013
John R. Koza. Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge, MA, USA, 1992
Hadas Kress-Gazit and Hazem Torfah. The challenges in specifying and explaining synthesized implementations of reactive systems. In Bernd Finkbeiner and Samantha Kleinberg, editors, Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology, Thessaloniki, Greece, 21st April 2018, volume 286 of Electronic Proceedings in Theoretical Computer Science, pages 50-64. Open Publishing Association, 2019
Jan Kretinsky, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for-words, automata, and LTL. In Automated Technology for Verification and Analysis-16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, pages 543-550, 2018
Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi A. Junttila. Simple bounded LTL model checking. In Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, pages 186-200, 2004
Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. Genprog: A generic method for automatic software repair. IEEE Trans. Softw. Eng., 38(1):54-72, January 2012
Jianwen Li, Geguang Pu, Lijun Zhang, Yinbo Yao, Moshe Y. Vardi, and Jifeng He. Polsat: A portfolio LTL satisfiability solver. CoRR, abs/1311.1602, 2013
Jianwen Li, Shufang Zhu, Geguang Pu, and Moshe Y Vardi. SAT-based explicit LTL reasoning. In Haifa Verification Conference, pages 209-224. Springer, 2015
Wenchao Li, Lili Dworkin, and Sanjit A Seshia. Mining assumptions for synthesis. In Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011), pages 43-50. IEEE, 2011
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag New York, Inc., New York, NY, USA, 1992
Zohar Manna and Amir Pnueli. Temporal verification of reactive systems: safety. Springer-Verlag New York, Inc., New York, NY, USA, 1995
Zohar Manna and Pierre Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst., 6(1):68-93, 1984
Shahar Maoz, Jan Oliver Ringert, and Rafi Shalom. Symbolic repairs for GR(1) specifications. In Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, pages 1016-1026, 2019
S. Mechtaev, J. Yi, and A. Roychoudhury. Directfix: Looking for simple program repairs. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 1, pages 448-458, 2015
Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! In Computer Aided Verification-30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, pages 578-586, 2018
Z. Michalewicz. Genetic Algorithms + Data Structures = Evolution Programs. Springer, 1996
Nir Piterman, Amir Pnueli, and Yaniv Sa?ar. Synthesis of reactive(1) designs. In VMCAI, pages 364-380, 2006
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ?89, pages 179-190, New York, NY, USA, 1989. ACM
Vasumathi Raman and Hadas Kress-Gazit. Explaining impossible high-level robot behaviors. Trans. Rob., 29(1):94-104, February 2013
Viktor Schuppan. Towards a notion of unsatisfiable cores for LTL. In Farhad Arbab and Marjan Sirjani, editors, Fundamentals of Software Engineering, pages 129-145, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg
Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. Ganak: A scalable probabilistic exact model counter. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19, pages 1169-1176. International Joint Conferences on Artificial Intelligence Organization, 7 2019
Marc Thurley. sharpsat-counting models with advanced component caching and implicit BCP. In Theory and Applications of Satisfiability Testing-SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, pages 424-429, 2006
Axel van Lamsweerde. Requirements Engineering-From System Goals to UML Models to Software Specifications. Wiley, 2009
Axel van Lamsweerde and Emmanuel Letier. Handling obstacles in goal-oriented requirements engineering. IEEE Trans. Softw. Eng., 26(10):978-1005, October 2000
Andras Vargha and Harold D. Delaney. A Critique and Improvement of the "CL" Common Language Effect Size Statistics of McGraw and Wong. Journal of Educational and Behavioral Statistics, 25(2):101-132, 2000
