a quiet coastal scene

yusuf ersel bal

formal methods for dependable software
and systems

i work as a software and test engineer at Siemens, on an industrial predictive maintenance platform. i write services that collect data from drives, PLCs and all kinds of industrial equipment, and the test infrastructure for them. i graduated in computer engineering at Bahcesehir University and i am finishing a double major in industrial engineering.

my long term interest is formal methods and programming languages for dependable software and systems. most of what i have done so far is on the testing side of that, and i am learning static analysis, symbolic execution and formal verification. i am particularly interested in how we can obtain useful, machine-checkable guarantees for software whose failures are difficult or costly to detect. i also try to read and reproduce papers in these areas when i have time, and i currently have two studies of my own prepared as preprints.

i am looking for funded research msc or mphil positions starting in september 2027. =)

background

i first took an associate degree in computer programming at Marmara University. i finished first in the department and second in the school, and transferred to Bahcesehir University through DGS, the national exam for transferring from an associate to a bachelor's degree, in which i ranked 234th.

i started at Bahcesehir University in industrial engineering with a full scholarship, then changed my major to computer engineering. later i took industrial engineering again as a double major. computer engineering is my main degree. both programmes are taught in English.

for about a year i led the software unit of an electric vehicle team for the TUBITAK efficiency challenge. i worked on telemetry, embedded integration and motor control.

i have been at Siemens since april 2025, in r&d, on digital drivetrain analyzer onsite. it is a distributed system of Go and C++ services running in containers on Debian, with gRPC and REST interfaces, sensor acquisition and time-series storage. i work on the services and on system-level test automation that runs against real industrial equipment.

research

most of my work so far has been testing, test automation and debugging. i want to move towards methods that give stronger guarantees, and i am learning static analysis, symbolic execution, SMT-based reasoning and formal verification. part of why this interests me is that i want important software to be checkable by a machine, whoever or whatever wrote it. the amount of generated code is growing quickly, which makes that kind of checking more useful, and compilers and code-generation tools are an obvious example, because errors in them can propagate into otherwise correct programs. stronger type systems, including dependently typed languages and Haskell, are one direction i am curious about, though it is a small part of what i work on.

the other question i keep coming back to is what guarantees remain possible when correct software runs on unreliable hardware or under difficult operating conditions. i am interested in silent data corruption and software fault tolerance for that reason. cyber-physical and embedded systems are one important application area for these questions, mainly because that is where much of my own experience comes from, through Siemens and the electric vehicle team. high-performance and scientific computing is another, since it shares the same concerns about correctness and unreliable hardware at scale.

i am also interested in optimisation and operations research, which is why i took the industrial engineering degree, although i have not done research in that area yet. for a master's i would also consider control, embedded and industrial software, distributed and edge systems, or optimisation. after that i would like to do a phd.

a diagram: formal methods and analysis, programming languages and theory, and testing and bug finding, used to obtain guarantees for compilers and code generation, embedded and cyber-physical systems, scientific and HPC systems, harsh and extreme environments, and databases and distributed systems.

i reproduce published work on my own. i build the artifact, run it under fixed resource limits, and write down what reproduced and what i could not reach. i do this when i find time. five of them so far, in areas including metamorphic testing, protocol verification and type inference. some of them are partial.

i also have two studies of my own, one on predictive monitoring under distribution shift and one on the robustness of a vision pipeline under changing operating conditions, currently prepared as preprints.

other things

i have an old compact digital camera and i take photographs with it. its battery does not hold a charge anymore and runs out about a minute after i turn it on. i have not replaced it yet =(. i like long walks, usually a whole day, in ordinary green areas and small villages rather than well known places. the areas around anadolu kavagi and rumeli feneri are next on the list. i grow plants and flowers. i also pick up plants when i see them outside, and i press and dry them. most of the photographs i take are of plants. i listen to kurdish music, mostly koma mezrabotan, koma nurhak, grup kizilirmak and rojda, and to a lot of indie and math rock, wang wen, chinese football, i'm fine! thank you! and you?, pocari sweet, chestnut bakery, my little airport, toe, advantage lucy, onsoku line, kent and sweet trip. for films i like made in hong kong, taste of cherry, dogville and mulholland drive, and the last one i watched was a separation. i have read faust and frankenstein more than once, and for manga and anime i like yokohama kaidashi kikou, kino no tabi and revolutionary girl utena. i hope to travel to iran, kazakhstan, kyrgyzstan, lebanon, morocco, china, vietnam, the philippines and spain.

the domain name comes from my little airport and from the yueqin that alpha plays in yokohama kaidashi kikou. the photograph at the top of the page is that scene.