Martin Lester 0001

dblp:72/7705-1 · also Martin Mariusz Lester · DBLP profile ↗
← Back
9ranked-venue papers
6as first author
6since 2021 · last 2026
0000-0002-2323-1771ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Artificial intelligence and machine learning · 4 · 1 first-author · 4 since 2021Software engineering, systems software and programming languages · 3 · 3 first-author · 2 since 2021Security and privacy · 2 · 2 first-authorTheory of computation · 1 · 1 first-author · 1 since 2021
YearPublicationVenuePosition
2026 BaB-PoNN: A Bit-Exact Branch-and-Bound Framework for Verified Robustness of Posit Neural Networks
Suleiman Junaidu Sadiq, Martin Lester 0001
CPAIOR2
2025 Fault Robustness and Lightweight Error Correction for Low-Precision Posit Neural Networks in Safety-Critical Systems
abstract
Low-precision neural networks are increasingly adopted in safety-critical systems where energy efficiency and computational speed are essential. Posit number systems, particularly posit-8 representations, offer favorable trade-offs between dynamic range and precision, but their resilience to hardware faults remains underexplored. This paper investigates the fault robustness of posit-8 neural networks in a safety-critical advisory setting using the Posit Flight Advisory Network (PFAN) model. We develop a fast bit-flip fault injection framework targeting posit-encoded weights and evaluate advisory failure rates under single-bit, adjacent, and burst faults across both low and high-density fault injection scenarios. To mitigate fault-induced errors, we integrate two protection mechanisms: Hamming (13,8) SEC-DED codes for weight-level correction and output-level Triple Modular Redundancy (TMR). Combined ECC and TMR protection eliminates all observed advisory errors under single-replica fault conditions, and reduces the residual failure rate under double-replica corruption to 0.08%. Zero-failure configurations yield a 95% confidence upper bound of 2.16 failures per hour assuming a 10 Hz inference rate. These results demonstrate that lightweight protection strategies can enable dependable deployment of posit-based neural networks in safety-critical AI applications.
Suleiman Junaidu Sadiq, Martin Lester 0001
ICMLA2
2024 Learning a Strategy for Preference Elicitation in Conversational Recommender Systems
abstract
This paper delves into the information elicitation aspect of Conversational Recommender Systems (CRS), presenting an innovative method of selecting chatbot questions that result in the highest information gain when reconstructing the preference profile of a user, which allows one to achieve high-quality recommendations after a small number of conversational interactions. The proposed system comprises a Recommendation Module and a Preference Elicitation Module. The Recommendation Module leverages a Long Short-Term Memory (LSTM) network with an Attention mechanism and is optimised to reconstruct the preference profiles of new users based on limited information gathered through dialogue. The Preference Elicitation Module is trained using a reinforcement learning technique known as bot-play, where the Questioner Bot proactively prompts the Answerer Bot to provide item and attribute ratings, leveraging the reduction in the Recommendation model’s loss as a reward signal. This enables the model to learn an optimal questioning strategy, thereby maximising the accuracy of the representation of the user profile and the relevance of recommendations. The experimental results demonstrate the ability of the Recommendation component to learn item-attribute mappings, enabling the Questioner Bot to make accurate rating predictions with only a limited number of answered questions. Moreover, the trained Preference Elicitation policy model consistently outperforms the baseline model across both synthetic and real-world datasets, showcasing its ability to minimise the number of conversational turns required to achieve accurate recommendations.
Aleksandra Makarova, Xia Hong 0001, Martin Lester 0001
IJCNN4
2024 Cutting the Cake into Crumbs: Verifying Envy-Free Cake-Cutting Protocols Using Bounded Integer Arithmetic
Martin Lester 0001
PADL1
2023 CoPTIC: Constraint Programming Translated Into C
abstract
Abstract Constraint programming systems allow a diverse range of problems to be modelled and solved. Most systems require the user to learn a new constraint programming language, which presents a barrier to novice and casual users. To address this problem, we present the CoPTIC constraint programming system, which allows the user to write a model in the well-known programming language C, augmented with a simple API to support using a guess-and-check paradigm. The resulting model is at most as complex as an ordinary C program that uses naive brute force to solve the same problem. CoPTIC uses the bounded model checker CBMC to translate the model into a SAT instance, which is solved using the SAT solver CaDiCaL. We show that, while this is less efficient than a direct translation from a dedicated constraint language into SAT, performance remains adequate for casual users. CoPTIC supports constraint satisfaction and optimisation problems, as well as enumeration of multiple solutions. After a solution has been found, CoPTIC allows the model to be run with the solution; this makes it easy to debug a model, or to print the solution in any desired format.
Martin Lester 0001
TACAS (2)1
2021 Scheduling Reach Mahjong Tournaments Using Pseudoboolean Constraints
Martin Lester 0001
SAT1
2019 Analysis of MiniJava programs via translation to ML
abstract
MiniJava is a subset of the object-oriented programming language Java. Standard ML is the canonical representative of the ML family of functional programming languages, which includes F# and OCaml. Different program analysis and verification tools and techniques have been developed for both Java-like and ML-like languages. Naturally, the tools developed for a particular language emphasise accurate treatment of language features commonly used in that language. In Java, this means objects with mutable properties and dynamic method dispatch. In ML, this means higher order functions and algebraic datatypes with pattern matching.
Martin Lester 0001
FTfJP@ECOOP1
2016 Information flow analysis for a dynamically typed language with staged metaprogramming
abstract
Web applications written in JavaScript are regularly used for dealing with sensitive or personal data. Consequently, reasoning about their security properties has become an important problem, which is made very difficult by the highly dynamic nature of the language, particularly its support for runtime code generation via eval. In order to deal with this, we propose to investigate security analyses for languages with more principled forms of dynamic code generation. To this end, we present a static information flow analysis for a dynamically typed functional language with prototype-based inheritance and staged metaprogramming. We prove its soundness, implement it and test it on various examples designed to show its relevance to proving security properties, such as noninterference, in JavaScript. To demonstrate the applicability of the analysis, we also present a general method for transforming a program using eval into one using staged metaprogramming. To our knowledge, this is the first fully static information flow analysis for a language with staged metaprogramming, and the first formal soundness proof of a CFA-based information flow analysis for a functional programming language.
Martin Lester 0001, C.-H. Luke Ong, Max Schäfer
J. Comput. Secur.1
2013 Information Flow Analysis for a Dynamically Typed Language with Staged Metaprogramming
abstract
Web applications written in JavaScript are regularly used for dealing with sensitive or personal data. Consequently, reasoning about their security properties has become an important problem, which is made very difficult by the highly dynamic nature of the language, particularly its support for runtime code generation. As a first step towards dealing with this, we propose to investigate security analyses for languages with more principled forms of dynamic code generation. To this end, we present a static information flow analysis for a dynamically typed functional language with prototype-based inheritance and staged metaprogramming. We prove its soundness, implement it and test it on various examples designed to show its relevance to proving security properties, such as noninterference, in JavaScript. To our knowledge, this is the first fully static information flow analysis for a language with staged metaprogramming, and the first formal soundness proof of a CFA-based information flow analysis for a functional programming language.
Martin Lester 0001, C.-H. Luke Ong, Max Schäfer
CSF1