报告标题：AgentOrchestrationwithTransitionSystemTheory报告时间：5月12日15：00-16：30报告地点：滴水湖国际软件学院502室报告摘要：Agent orchestration has emerged as a centralchallenge in building reliable multi-agentsystems, especially when complex tasks requirecoordination, adaptation, and verifiableexecution. We present a transition-

报告标题：The deal with Design by Contract and why it is worth the fuss报告时间：5月13日13：30-15：00报告地点：理科大楼B211报告摘要：Design by Contract is a discipline of software construction -- requirements, design, implementation, testing, proofs, documentation, management -- which profoundly changes the way we look at soft

报告标题：智能软件系统的缺陷测试与修复报告时间：5月6日15：00-17：00报告地点：数学馆201报告摘要：功能错误是移动应用软件（简称移动应用）中最常见的一类错误，可能导致严重的后果。然而，功能错误检测对手动和自动化测试而言皆具挑战性。基于性质的测试方法融合人工测试的知识优势与自动化测试的低成本优势，在移动应用功能测试中展现重要价值，但仍存在尚未解决的关键难题。为此，报告人进行了一系列研究，旨在解决现有技术存在的性质定义和错误定位难的问题。报告人首先提出跨应用的抽象性质定义方法，允许刻画功能在不同移动应用中应遵守的性质。此外，分别提出了基于性质的自动化功能错误检测与定位方法，可在移动应用中

报告标题：基于性质的移动应用功能测试研究报告时间：4月30日17：00-18：00报告地点：理科大楼B1014报告摘要：功能错误是移动应用软件（简称移动应用）中最常见的一类错误，可能导致严重的后果。然而，功能错误检测对手动和自动化测试而言皆具挑战性。基于性质的测试方法融合人工测试的知识优势与自动化测试的低成本优势，在移动应用功能测试中展现重要价值，但仍存在尚未解决的关键难题。为此，报告人进行了一系列研究，旨在解决现有技术存在的性质定义和错误定位难的问题。报告人首先提出跨应用的抽象性质定义方法，允许刻画功能在不同移动应用中应遵守的性质。此外，分别提出了基于性质的自动化功能错误检测与定位方法，可在

报告标题：Toward Efficient Verification of the Finite Variant Property报告时间：4月21日14：00-15：30报告地点：理科大楼B1002报告摘要：Modern security protocols are used everywhere, from online banking and messaging apps to digital authentication systems. To ensure that these protocols are secure, researchers often rely on forma

报告标题：Tuning into my heart through wearables: towards a formal cardiac digital twin报告时间：1月4日13：00报告地点：理科大楼B211报告摘要：Digital Twins (DTs) mimic a physical system using a digital version of the real system. While these have been explored in many domains,digital twins of human organs are yet to be created