Manzino and de Latorre present a Haskell-embedded DSL that enforces Delimited Release by encoding security policies in types, reducing to type-checking verification. It is evaluated via three examples: purchase, database access, and password checking.

Passato et al. present DEScMaker to automatically generate C or structured code from SCT-based FSM controllers, preserving properties like controllability and non-blockingness. Its effectiveness is shown through examples comparing it to manual coding.

Lourenço and Pinto present Why3-do for auto-active verification of distributed algorithms supporting specification refinement and extension for specific classes. The evaluation includes a verified gallery of distributed algorithms, e.g., Paxos consensus.

Cruz et al. employ continuous feedback to enhance ML-based code smell detection. They compare detection performance before and after iterative expert-like feedback on 4 code smells on 20 Java systems, showing notable accuracy and F1-score improvements.

De Palma et al. incorporate tAPP, a declarative language for expressing topology-aware scheduling policies in OpenWhisk. In a case study across multiple cloud regions, tAPP reduces latency and performance variability compared to standard OpenWhisk.

Scott and Johnstone introduce a modified version of Earley's general parsing algorithm that employs a precomputed table to improve efficiency. On Java and ANSI C, it shows less memory usage and efficiency than the traditional Earley parser.

Belghiat presents a method to assign formal semantics to UML2 sequence diagrams via translation into π-calculus. It enables systematic construction and reasoning of complex behaviors through a case study with the MWB tool for formal verification.

Aracena et al. propose an LLM-based method for automating issue classification, with less need for large training data. Evaluation on NLBSE 2023 and 2024 datasets revealed that fine-tuned GPT-4o outperformed DeepSeek R1, achieving an average 80.7% F1.

Li et al. introduce ESBMC v7.6, an enhanced SMT-based model checker for C++ that builds on the Clang-based front-end of ESBMC v7.3. It supports exception handling, improved memory safety analysis, and updated STL operational models using Clang AST.

Protim Roy et al. investigate the use of Software Project Management Tools in Bangladesh's IT industry. A survey of 87 software companies revealed that about half use such tools, with Jira on top, and ten frequently used functionalities.

Roßbach and Leuschel introduce a certified control framework for YOLO-based train sign classification, enabling formal safety guarantees. Results are promising, but further research is needed to generalize certified control for other tasks.

Lee et al. introduce STLmc to reduce robust STL model checking for hybrid systems to first-order logic satisfiability. The effectiveness of STLmc is shown on a number of hybrid system case studies.

Zhang et al. evaluate EvoMaster, a web service test generator, within microservice systems at Meituan for 2 years in 3 user studies. EvoMaster enhances code coverage and fault detection in microservices, driving its use in Meituan's testing pipeline.

Stradowski and Madeyski examine false positives in ML defect prediction, emphasizing their negative impact on developer trust and adoption. The approach was used in Nokia 5G’s implementation, focusing on human acceptance and business value alignment.

Aburakhia and Alshayeb prioritize third-party libraries in mobile apps based on five categories. Using AHP and SAW decision-making with a chatbot, the approach was evaluated with 7 developers; 82% found it useful, greatly reducing task completion time.

Choma and Zaina review the literature on the quality aspects considered in the UX evaluation of IoT applications in smart cities. 43 studies revealed a gap in non-traditional interfaces and smart technologies in specific interaction contexts.

González and Cernuzzi add an Architecture Specific Model (ASM) layer in MoWebA to improve adaptability across architectures. This is validated through extensions to three architectures, analysis of model independence and automation, and user feedback.

Mu et al. introduce a method to test reduce function commutativity with multi-column inputs using symbolic execution, dynamic slicing, and record permutations. Experiments confirm its effectiveness and the efficiency of the Gm permutation strategy.

Bachiri et al. propose a formal verification method for quantized neural networks in autonomous vehicles using SMT-based analysis of perturbed rational approximations. The approach is evaluated using the Highway-env simulator and Z3 SMT solver.

Lehmann et al. introduce a provably safe online strategy synthesis for needle steering in medical robotics by modeling the problem as a timed game. The method ensures safety guarantees and practical performance, demonstrated in medical simulations.