جست‌وجوی استاد و پژوهشگر

Ali Hamieمشاهده پروفایل

مدرس ارشد

• Formal Aspects of Software Development
• Software Engineering
• Formal Methods
• +۴ مورد دیگر

Ali Hamie is a Senior Lecturer at the School of Architecture, Technology and Engineering (University of Brighton, UK), specializing in formal methods in software engineering and ontology modeling. With over 35 publications, his work bridges theoretical formalisms like UML, OCL, and JML with practical implementation validation. BSc in Pure Mathematics (Lebanese University, 1982) Postgraduate Diploma in Computing (University of Essex, 1986) MSc in Computer Science (University of Essex, 1987) PhD in Computer Science (University of Essex, 1991) His research focuses on formal aspects of software development , including specification patterns, design by contract, and translation between formal notations (OCL to JML). Recent work examines diagrammatic reasoning in ontology engineering and hybrid modeling approaches combining formal and agile methods. Studies show his publications span formal methods , ontology modeling , and constraints validation , with recurring themes in OCL-JML interoperability, diagrammatic notations, and user-centric formalism evaluation. Awards include Fellow of the Higher Education Academy (2017) . He supervises research in formal computing, with past topics covering concept diagrams and ontology modeling. His academic career includes postdoctoral roles at Newcastle University and EPSRC-funded work at Imperial College.

Yoonsik Cheonمشاهده پروفایل

دانشیار

• Formal Methods
• Software Testing
• Programming Languages
• +۳ مورد دیگر

Yoonsik Cheon is an Associate Professor in the Department of Computer Science at the University of Texas at El Paso (UTEP), part of the College of Engineering. His research focuses on formal methods, software engineering, and mobile applications. He holds a Ph.D. from Iowa State University and has prior industry experience at the Electronics and Telecommunications Research Institute (ETRI) in South Korea. His work emphasizes operational formal methods, integrating specifications like JML and CleanJava into practical development processes. Research Interests: Formal methods (specification languages, verification techniques), programming languages, mobile application development, and software testing. His Software Specification and Verification Lab explores automated testing, functional program verification, and applying formal methods to mobile apps. Key Achievements: Recipient of the 2022 AITO Test of Time Award for his foundational work on JML and JUnit integration. He has contributed to tools like the JML runtime assertion checker and CleanJava for functional verification. His publications frequently address design constraints, assertion-based testing, and cross-platform development strategies. Teaching: Courses include Programming Languages, Mobile Application Development, and formal methods in software engineering.

Jinting Bianمشاهده پروفایل

پژوهشگر

• Formal Verification
• Software Verification
• Object-Oriented Programming
• +۹ مورد دیگر

Jinting Bian is a Researcher at the Computer Security department of Centrum Wiskunde & Informatica (CWI), Amsterdam, The Netherlands . Their work focuses on formal verification , object-oriented programming , and software correctness . Research Interests include: Formal verification of object-oriented systems History-based reasoning for behavioral subtyping Dynamic frames and footprint logic Java Collection Framework specification Integration of Isabelle/HOL with KeY Interactive deductive proving Publications between 2020-2025 demonstrate expertise in Hoare logic , behavioral subtyping , and Java standard library verification . Key collaborations include Frank de Boer , Hans-Dieter Hiep , and Stijn de Gouw .

Clyde Rubyمشاهده پروفایل

دانشیار

• Programming Language Semantics
• Object-Oriented Programming
• Programming Methodology
• +۴ مورد دیگر

Clyde Ruby is an Associate Professor of Computer Science at Iowa State University. He holds a PhD from Iowa State University (2006) and prior degrees from Maharishi International University (BA, MA, MS). His research focuses on programming language semantics, particularly in object-oriented contexts, specification languages like JML and Larch/C++, and verification methodologies. Ruby has contributed to foundational work on subclass verification and formal software specification frameworks. Education: PhD in Computer Science, Iowa State University (2006) MS in Computer Science, Maharishi International University MA and BA from Maharishi International University Ruby’s research emphasizes ensuring software correctness through formal methods, including modular subclass verification and the design of behavioral interface specifications (e.g., JML). His work bridges theory and practice, aiming to enhance software reliability and maintainability. He has published extensively on topics like specification languages, formal verification, and object-oriented programming principles. His research trends include advancing specification frameworks for Java (JML), exploring formal methods for runtime assertion checking, and improving subclass verification techniques without superclass code access. These efforts contribute to safer and more precise software development practices. Ruby has collaborated on significant projects like the Java Modeling Language (JML) and Larch/C++. While no awards are explicitly listed, his impactful contributions to formal methods are evident through his publications in top venues like ACM SIGSOFT and Science of Computer Programming. He leads the JML project and contributes to Larch-related initiatives, focusing on bridging formal specifications with practical software engineering workflows.

• Materials Science
• Phase Transformations
• Neutron Scattering
• +۴ مورد دیگر

Monika Rolinska is a doctoral student and Researcher at KTH Royal Institute of Technology since April 2021, affiliated with the HULTGREN LABORATORY. She is part of the Swedish graduate school on neutron scattering (SwedNess), focusing on nucleation in metallic materials using in-situ neutron and X-ray scattering to develop computational frameworks for phase transformation modeling. She also serves as a course assistant for MH1030 Material Design I and contributes to the MSE's JML group. Education: Master of Science in Materials Design (KTH), with a BSc thesis on additive manufacturing of carbon fibers in steel matrices and an MSc thesis on extraction replicas for precipitate analysis, both in collaboration with Swerim AB. Research interests center on phase transformations, nucleation theory limitations, and integrating experimental data with ab initio calculations for materials design. Her work bridges materials science, scattering techniques, and computational modeling. Labs/Teams: Active in the HULTGREN LABORATORY and MSE's JML group. Collaborates with Swerim AB on applied materials analysis.

• Human-Computer Interaction
• Interaction Design
• Feminist Technology
• +۷ مورد دیگر

Marianela Ciolfi Felice is a tenure-track Assistant Professor in Interaction Design at KTH Royal Institute of Technology, within the Department of Media Technology and Interaction Design under the School of Electrical Engineering and Computer Science. Her work bridges critical feminist computing, AI, and soma design, focusing on technology's role in addressing societal inequalities. Key Affiliation: KTH Royal Institute of Technology Department: Media Technology and Interaction Design Research Focus: Critical Feminist Computing, AI Ethics, Soma Design, Intimate Technologies Her research explores body-centered technologies across life transitions such as menstruation, menopause, and contraception, challenging medicalization frameworks and advocating for marginalized communities. She has received 7 Best Paper awards and 4 Honorable Mentions at ACM CHI and DIS conferences. Current projects include AymurAI (feminist AI for Latin American judicial reform) and collaborations with DataGénero NGO. She supervises PhD students and contributes to gender equality initiatives through EECS school's JML work group. Best Paper Award, ACM CHI 2025 Honorable Mention Award, ACM DIS 2025

Christine Paulin-Mohringمشاهده پروفایل

استاد

• Program verification
• Type theory
• Interactive theorem proving
• +۵ مورد دیگر

Christine Paulin-Mohring is a Full Professor at Université Paris-Saclay's Faculty of Science since 1997. She previously held a secondment at INRIA Futurs/Saclay Île-de-France (2006-2008), was a CNRS Researcher at ENS Lyon (1989-1997), and an assistant professor at ENS Paris (1985-1989). She earned her PhD in 1989 from Université Paris 7 under Gérard Huet's supervision at INRIA Rocquencourt and ENS Paris. Her research focuses on Program verification Type theory Interactive theorem proving Formal methods Coq proof assistant Randomized algorithms She has developed the ALEA Coq library for randomized programs and led the ProVal research group until 2011. Her award highlights include ACM Software System Award (2013) Doctor Honoris Causa from University of Gothenburg (2011) Prix Michel Monpetit (2015) Academia Europaea membership (2014) She has advised 15 PhD students and coordinated major projects like DigiCosme Labex (2007-2011). Her administrative roles include Dean of the Faculty of Science (2016-2021) and leadership in doctoral schools.

Mattias Ulbrichمشاهده پروفایل

پژوهشگر ارشد

• Formal software verification
• Relational verification
• Regression verification
• +۷ مورد دیگر

Dr. Mattias Ulbrich is a Research Fellow at the Institute of Information Security and Dependability (KASTEL) within the Department of Informatics at Karlsruhe Institute of Technology (KIT). His primary research focus lies in formal deductive software verification at the program code level, with special emphasis on relational verification where multiple programs are considered simultaneously. His work spans regression verification, equivalence checking, algorithm refinement, and verification of relational properties of algorithms. His research interests include formal software verification, relational verification techniques, program equivalence checking, information flow security, and intermediate verification languages. Ulbrich has made significant contributions to the KeY project, an integrated deductive software design tool, and has developed various verification tools including rêve for program equivalence checking and SemSlice for precise program slicing. His work bridges theoretical foundations with practical applications in software verification. Analysis of his recent publications reveals a strong trend toward practical applications of formal verification methods, particularly in industrial contexts like automated production systems. His work increasingly focuses on usability of verification tools, integration of different verification paradigms, and application to real-world software systems including JDK components. There's also growing interest in educational aspects of formal methods, as seen in his work on introducing algorithmic thinking to younger students. Ulbrich has supervised numerous Master's and Bachelor's theses across a wide range of verification topics, demonstrating his commitment to mentoring the next generation of formal methods researchers. His teaching activities include courses on formal systems and verification at KIT, with particular focus on teacher education programs in computer science. He is actively involved in the formal methods community, serving on program committees for major conferences including VSTTE, VerifyThis, and ISoLA. Ulbrich has been a steering committee member for VerifyThis since 2019 and has co-organized several workshops and Dagstuhl seminars focused on program equivalence and relational verification.

• Formal Verification
• Model Checking
• Parity Games
• +۵ مورد دیگر

Tom van Dijk serves as an Assistant Professor in the Formal Methods and Tools group at the University of Twente, where he conducts cutting-edge research in formal verification and develops practical software tools for the verification community. His work bridges theoretical computer science with real-world applications in model checking and synthesis. His educational background includes: PhD in Computer Science (2016), University of Twente. Thesis: Sylvan: Multi-core Decision Diagrams MSc in Computer Science (2012, cum laude), University of Twente. Thesis: The parallelization of binary decision diagram operations for model checking BSc in Computer Science (2010), University of Twente. Thesis: Analysing And Improving Hash Table Performance Van Dijk's research centers on formal verification with specialization in parity games and binary decision diagrams . He pioneers multi-core parallel algorithms for symbolic model checking, focusing on practical implementations that scale to industrial problems. His work integrates SAT/SMT solving , reactive synthesis , and algorithm optimization to advance the state-of-the-art in verification tooling. His publication trajectory reveals consistent innovation in parity game solving, evolving from foundational work on tangle-based algorithms to recent contributions in reproducibility and AI-aided verification. The 2024 papers demonstrate expanding scope into educational technology while maintaining core focus on game-solving efficiency and synthesis techniques. His key recognitions include: Dutch national M&I Informatie Scriptieprijs 2012 (2nd place) for MSc thesis Best paper award at SPIN 2017 for distributed BDD research Van Dijk actively mentors students and seeks collaborations: Student Supervision : Welcomes BSc/MSc students for projects on parity games and BDDs Tool Development : Maintains open-source research tools (Sylvan, Oink, Knor) Community Service : Serves on 20+ program committees including CAV and TACAS As core member of the Formal Methods and Tools group, he contributes to major verification frameworks including LTSmin, Storm, and IscasMC. His Lace work-stealing framework underpins parallelization in multiple verification tools, while ongoing projects focus on polynomial-time parity game solutions and AI integration in verification workflows.

• Employment Law
• Labor Law
• Discrimination Law
• +۵ مورد دیگر

Karina Godoy is an Adjunct Professor at Southwestern Law School, teaching the Employment Law Survey Course. She is an associate attorney at JML Law, specializing in employment law, including discrimination, wage and hour disputes, whistleblowing, wrongful termination, and labor litigation. She joined Southwestern in 2020. Education: B.A. (summa cum laude) in History and Political Science from the University of Southern California (2006); J.D. from Southwestern Law School (2015), graduating in the top 10% of her class. Recognized on the Dean’s List and for academic excellence, she received the Witkin Award for Labor Law. Professional Experience: Handles litigation phases from client vetting to trials. Externships included the Immigration Law Clinic, Honorable Terry J. Hatter Jr.’s judiciary, EEOC, and Bet Tzedek’s Wage and Hour Clinic. Previously an ABOTA Fellow at a defense firm, she now focuses on employee representation. Awards: Named a 'Super Lawyer - Rising Star' (2019–2020). Honored with scholarships and accolades for pro bono work (over 500 hours) and public service. Community Involvement: Vice-Chair of the Workers Outreach Committee and Treasurer of the Whittier Bar Association. Active with Bet Tzedek’s Workers’ Rights Clinic and takes pro bono cases.

• Soil Science
• Pedology
• Soil Health
• +۳ مورد دیگر

Zachary Smith is a Research Specialist at the Department of Soil and Water Systems within the University of Idaho's College of Agricultural and Life Sciences. He can be contacted at zsmith@uidaho.edu or via phone at 509-378-0698 from Room 81C of JML. His research focuses span Soil Science Pedology Soil Health Agricultural Systems Water Management . The department's associated programs include the Pedology Laboratory, Soil and Land Evaluation Program, and Soil Health initiatives.

Yves Ledruمشاهده پروفایل

استاد

• Software Engineering
• Formal Methods
• Specification and Modeling
• +۵ مورد دیگر

Yves Ledru is a Professor at UFR IM2AG of Université Grenoble Alpes (formerly Université Joseph Fourier), where he also serves as Deputy Director. He is a member of the Laboratoire d'Informatique de Grenoble (LIG) and heads the VASCO research team. Additionally, he serves on the bureau of the GDR GPL national research group of the CNRS. Professor Ledru's research focuses on Software Engineering and Formal Methods. His primary interests include Specification and Modeling, Software Architecture, Testing, and the application of formal specification languages such as JML, VDM, and Z Notation. His team has developed several tools including RoZ (for integrating UML and Z specifications), B4MSecure, Tobias (for combinatorial testing), and ParTraP. His recent research projects include ANR Philae (2018-2022), ANR MODMED (2015-2019), and NExTRegio project of IRT Railenium (2015-2019). Professor Ledru has been actively involved in the academic community, serving on program committees for numerous conferences including Crisis 2024, MEDI 2023, and RSSRail 2023. He was a member of the steering committee of the ASE conference from 1997 to 2013, serving as chair from 2001 to 2007. His publication record shows a consistent focus on bridging formal methods with practical software engineering applications, particularly in specification languages and testing methodologies. He has supervised twelve PhD students to completion and currently supervises Alexandre Monnier. His former administrative responsibilities include leading the ISLE research cluster of the Rhône-Alpes Region (2007-2011) and serving as scientific responsible for the ARC6: Technologies de l'Information et de la Communication (2011-2017).