publications
publications in reversed chronological order.
2024
-
-
- An Analysis of the Impact of Field-Value Instance Navigation in Alloy’s Model FindingIn Rigorous State-Based Methods - 10th International Conference, ABZ 2024, Bergamo, Italy, June 25-28, 2024, Proceedings, 2024
- SpecBCFuzz: Fuzzing LTL Solvers with Boundary ConditionsIn Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, ICSE 2024, Lisbon, Portugal, April 14-20, 2024, 2024
2023
-
- ACoRe: Automated Goal-Conflict ResolutionIn Fundamental Approaches to Software Engineering - 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, 2023
- Efficient Bounded Exhaustive Input Generation from Program APIsIn Fundamental Approaches to Software Engineering - 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, 2023
- Automated Repair of Unrealisable LTL Specifications Guided by Model CountingIn Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2023, Lisbon, Portugal, July 15-19, 2023, 2023
- Enabling Efficient Assertion InferenceIn 34th IEEE International Symposium on Software Reliability Engineering, ISSRE 2023, Florence, Italy, October 9-12, 2023, 2023
- Precise Lazy Initialization for Programs with Complex Heap InputsIn 34th IEEE International Symposium on Software Reliability Engineering, ISSRE 2023, Florence, Italy, October 9-12, 2023, 2023
- EvoSpex: A Search-Based Tool for Postcondition InferenceIn Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023, 2023
- SpecFuzzer: A Tool for Inferring Class Specifications via Grammar-Based FuzzingIn 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023, Luxembourg, September 11-15, 2023, 2023
2022
- Fuzzing Class SpecificationsIn 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022, 2022
- Learning to Prune Infeasible Paths in Generalized Symbolic ExecutionIn IEEE 33rd International Symposium on Software Reliability Engineering, ISSRE 2022, Charlotte, NC, USA, October 31 - Nov. 3, 2022, 2022
- ATR: template-based repair for Alloy specificationsIn ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022, 2022
- ICEBAR: Feedback-Driven Iterative Repair of Alloy SpecificationsIn 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022, 2022
- LISSA: Lazy Initialization with Specialized Solver AidIn 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022, 2022
2021
- Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field BoundsIn Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, 2021
- Artifact of ’FLACK: Counterexample-Guided Fault Localization for Alloy Models’In 43rd IEEE/ACM International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2021, Madrid, Spain, May 25-28, 2021, 2021
- EvoSpex: An Evolutionary Algorithm for Learning Postconditions (artifact)In 43rd IEEE/ACM International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2021, Madrid, Spain, May 25-28, 2021, 2021
- Artifact of Bounded Exhaustive Search of Alloy Specification RepairsIn 43rd IEEE/ACM International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2021, Madrid, Spain, May 25-28, 2021, 2021
- FLACK: Counterexample-Guided Fault Localization for Alloy ModelsIn 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021, 2021
- Bounded Exhaustive Search of Alloy Specification RepairsIn 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021, 2021
- EvoSpex: An Evolutionary Algorithm for Learning PostconditionsIn 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021, 2021
- BeAFix: An Automated Repair Tool for Faulty Alloy ModelsIn 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021, 2021
- FLACK: Localizing Faults in Alloy ModelsIn 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021, 2021
2019
- Satisfiability Calculus: An Abstract Formulation of Semantic Proof SystemsFundam. Informaticae, 2019
- An evolutionary approach to translating operational specifications into declarative specificationsSci. Comput. Program., 2019
- Automatically Identifying Sufficient Object Builders from Module APIsIn Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, 2019
- Training binary classifiers as data structure invariantsIn Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, May 25-31, 2019, 2019
- Efficient Test Generation Guided by Field Coverage CriteriaIn 34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019, San Diego, CA, USA, November 11-15, 2019, 2019
2018
- Automated workarounds from Java program specifications based on SAT solvingInt. J. Softw. Tools Technol. Transf., 2018
- Improving lazy abstraction for SCR specifications through constraint relaxationSoftw. Test. Verification Reliab., 2018
- From operational to declarative specifications using a genetic algorithmIn Proceedings of the 11th International Workshop on Search-Based Software Testing, ICSE 2018, Gothenburg, Sweden, May 28-29, 2018, 2018
- On the effect of object redundancy elimination in randomly testing collection classesIn Proceedings of the 11th International Workshop on Search-Based Software Testing, ICSE 2018, Gothenburg, Sweden, May 28-29, 2018, 2018
- Goal-conflict likelihood assessment based on model countingIn Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, 2018
- A genetic algorithm for goal-conflict identificationIn Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, 2018
2017
-
- Automated Workarounds from Java Program Specifications Based on SAT SolvingIn Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, 2017
- Efficient SAT-Based Software Analysis: From Automated Testing to Automated Verification and RepairIn 5th IEEE/ACM International FME Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2017, Buenos Aires, Argentina, May 27, 2017, 2017
- An Analysis of the Suitability of Test-Based Patch Acceptance CriteriaIn 10th IEEE/ACM International Workshop on Search-Based Software Testing, SBST@ICSE 2017, Buenos Aires, Argentina, May 22-23, 2017, 2017
- DynAlloy analyzer: a tool for the specification and analysis of alloy models with dynamic behaviourIn Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, 2017
- CLTSA: labelled transition system analyser with counting fluent supportIn Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, 2017
2016
- Goal-conflict detection based on temporal satisfiability checkingIn Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, 2016
- Algebraic Foundations for Specification RefinementsIn Formal Methods: Foundations and Applications - 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings, 2016
- An Evolutionary Approach to Translate Operational Specifications into Declarative SpecificationsIn Formal Methods: Foundations and Applications - 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings, 2016
- Field-exhaustive testingIn Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016, 2016
2015
-
- BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT SupportIEEE Trans. Software Eng., 2015
- Specifying Event-Based Systems with a Counting Fluent Temporal LogicIn 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1, 2015
- syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic SpecificationsIn Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, 2015
2014
-
- An experiment on teaching coordination in a globally distributed software engineering classIn 27th IEEE Conference on Software Engineering Education and Training, CSEE&T 2014, Klagenfurt, Austria, April 23-25, 2014, 2014
- Efficient Tight Field Bounds Computation Based on Shape PredicatesIn FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014
- Automated goal operationalisation based on interpolation and SAT solvingIn 36th International Conference on Software Engineering, ICSE ’14, Hyderabad, India - May 31 - June 07, 2014, 2014
- A Heterogeneous Characterisation of Component-Based System Design in a Categorical SettingIn Theoretical Aspects of Computing - ICTAC 2014 - 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, 2014
- Bounded exhaustive test input generation from hybrid invariantsIn Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, 2014
- Proceedings First Latin American Workshop on Formal Methods, LAFM 2013, Buenos Aires, Argentina, August 26th 20132014
2013
- Synthesizing Masking Fault-Tolerant Systems from Deontic SpecificationsIn Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, 2013
- Analyzing formal requirements specifications using an off-the-shelf model checkerIn 2013 XXXIX Latin American Computing Conference (CLEI), Caracas (Naiguata), Venezuela, October 7-11, 2013, 2013
- Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT SolvingIn Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, March 18-22, 2013, 2013
- Characterizing Fault-Tolerant Systems by Means of Simulation RelationsIn Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings, 2013
- Ranger: Parallel analysis of alloy models by range partitioningIn 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA, November 11-15, 2013, 2013
- Bounded Lazy InitializationIn NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, 2013
- Parallel Bounded Verification of Alloy Models by TranScopingIn Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers, 2013
2012
- A Categorical Approach to Structuring and Promoting Z SpecificationsIn Formal Aspects of Component Software, 9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12-14, 2012. Revised Selected Papers, 2012
- Model Checking Propositional Deontic Temporal Logic via a \(μ\)-Calculus CharacterizationIn Formal Methods: Foundations and Applications - 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings, 2012
- Specifying and Verifying Declarative Fluent Temporal Logic Properties of WorkflowsIn Formal Methods: Foundations and Applications - 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings, 2012
- Using Coverage Criteria on RepOK to Reduce Bounded-Exhaustive Test SuitesIn Tests and Proofs - 6th International Conference, TAP@TOOLS 2012, Prague, Czech Republic, May 31 - June 1, 2012. Proceedings, 2012
- Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General LogicsIn Recent Trends in Algebraic Development Techniques, 21st International Workshop, WADT 2012, Salamanca, Spain, June 7-10, 2012, Revised Selected Papers, 2012
2011
- Teaching software engineering using globally distributed projects: the DOSE courseIn Proceedings of the 2011 Community Building Workshop on Collaborative Teaching of Globally Distributed Software Development, CTGDSD 2011, Waikiki, Honolulu, HI, USA, May 21-28, 2011, 2011
- dCTL: A Branching Time Temporal Logic for Fault-Tolerant System VerificationIn Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings, 2011
- Incorporating Coverage Criteria in Bounded Exhaustive Black Box Test Generation of Structural InputsIn Tests and Proofs - 5th International Conference, TAP@TOOLS 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings, 2011
- Abstraction Based Automated Test Generation from Formal Tabular Requirements SpecificationsIn Tests and Proofs - 5th International Conference, TAP@TOOLS 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings, 2011
2010
- Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical SettingIn Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings, 2010
2009
- An introductory course on programming based on formal specification and program calculationACM SIGCSE Bull., 2009
- Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)AlloyIn Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, 2009
- Specifying and Verifying Business Processes Using PPMLIn Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings, 2009
2008
- Towards Abstraction for DynAlloy SpecificationsIn Formal Methods and Software Engineering, 10th International Conference on Formal Engineering Methods, ICFEM 2008, Kitakyushu-City, Japan, October 27-31, 2008. Proceedings, 2008
2007
-
- Design in CommUnity with Extension MorphismsIn Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, 2007
- Verifying Temporal Properties of CommUnity DesignsIn Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings, 2007
2006
- Extension Morphisms for CommUnityIn Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, 2006
2005
- Reasoning about static and dynamic properties in alloy: A purely relational approachACM Trans. Softw. Eng. Methodol., 2005
- Towards Dynamically Communicating Abstract Machines in the B MethodIn Formal Methods and Software Engineering, 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005, Proceedings, 2005
- DynAlloy: upgrading alloy with actionsIn 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, 2005
2004
- A logical basis for the specification of reconfigurable component based systemsKing’s College London, UK, 2004
- An Equational Calculus for AlloyIn Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings, 2004
- Implementing Dynamic Aggregations of Abstract Machines in the B MethodIn Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings, 2004
- Hierarchical Temporal Specifications of Dynamically Reconfigurable Component Based SystemsIn Proceedings of the First International Workshop on Formal Foundations of Embedded Software and Component-based Software Architectures, FESCA@ETAPS 2004, Barcelona, Spain, April 3, 2004, 2004
2003
- Some Institutional Requirements for Temporal Reasoning on Dynamic Reconfiguration of Component Based SystemsIn Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, 2003
- A Logical Basis for the Specification of Reconfigurable Component-Based SystemsIn Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, 2003
- Taking Alloy to the MoviesIn FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, 2003
- Towards Dynamic Population Management of Abstract Machines in the B MethodIn ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings, 2003
2002
- A Temporal Logic Approach to the Specification of Reconfigurable Component-Based SystemsIn 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 23-27 September 2002, Edinburgh, Scotland, UK, 2002