My Research Record: From Formal Verification to QGI

If you search for my academic work you will not find it under “Sam Sammane”. It is indexed under my legal name, Ghiath Al Sammane, sometimes written “Ghiath Al-Sammane” or “G. Al Sammane”. This page exists so that the two names, the publication record and the companies I run today are connected in one place, with persistent identifiers that anyone, human or machine, can verify.

Identifiers

• ORCID: 0009-0005-2864-729X
• Google Scholar: v2A_UIwAAAAJ
• DBLP: 15/3160
• ResearchGate: Ghiath Al-Sammane
• Doctorate: PhD in Nanotechnology (formal verification and automated reasoning), Université Joseph-Fourier – Grenoble I, 2005

What the work was about

Between 2002 and 2015 I worked on one problem from several directions: how to prove, rather than merely test, that a hardware design does what its specification says. Digital circuits had formal methods by then. Analog and mixed-signal (AMS) designs, the parts of a chip that deal with continuous voltages, oscillators, phase-locked loops and data converters, did not. Simulation could show a design working on a few thousand inputs. It could not show it working on all of them.

The methods in these papers attack that gap:

• Symbolic simulation replaces concrete input values with symbols and carries the algebra through the circuit, so one run stands for a whole family of behaviours.
• Interval arithmetic bounds the continuous quantities, so a proof holds for every value inside the bounds rather than for sampled points.
• Theorem proving in HOL (higher-order logic) turns the verification into a machine-checked proof.
• Multiway decision graphs (MDGs) give a compact way to represent and reason about systems with data, and combining them with SAT solving or HOL induction made the reachability analysis tractable.
• Run-time verification monitors a simulation against formal properties when a full proof is out of reach.

The earliest work, in Grenoble, was on simulation infrastructure itself: TheoSim (2004), a symbolic simulator, and the formal design of on-chip networking. The 2007 to 2009 papers, written with Mohamed Zaki, Sofiène Tahar, Guy Bois, Sa’ed Abed and Otmane Ait Mohamed among others, applied these methods to real AMS blocks: delta-sigma modulators, PLLs, and VHDL-AMS models. The 2013 journal article and the 2015 Springer chapter consolidated the approach.

Why it matters for what I build now

TheoSym takes its name from TheoSim, the 2004 symbolic simulator. The idea carried over is the same: do not trust a system because it behaved well on the cases you happened to try. Represent its behaviour symbolically and reason about all of it.

QGI (Quantum General Intelligence) is built around symbolic reasoning, formal verification and theorem proving as the way to make AI agents accountable. An agent that acts on a business process should be verifiable in the same sense a circuit is: against a specification, with a trace that can be checked. That position is not a marketing line adopted in 2025. It is the research program above, applied to software agents instead of silicon.

Qalitex, the analytical testing laboratory, is the same discipline in a different form: a measurement is only worth something when the method behind it is documented, bounded and reproducible.

Publication list on ORCID (18 records, 17 distinct works)

Each entry links to the DOI. Author lists are as recorded by Crossref.

2015

1. Zaki, M. H., Hasan, O., Tahar, S., Al-Sammane, G. Framework for Formally Verifying Analog and Mixed-Signal Designs. In: Computational Intelligence in Analog and Mixed-Signal (AMS) and Radio-Frequency (RF) Circuit Design, Springer. 10.1007/978-3-319-19872-9_5

2013

2. Abed, S., Ait Mohamed, O., Al Sammane, G. Automatic verification of reduction techniques in Higher Order Logic. Formal Aspects of Computing. 10.1007/s00165-012-0223-x

2009

3. Wang, Z., Abbasi, N., Narayanan, R., Zaki, M. H., Al Sammane, G., Tahar, S. Verification of analog and mixed signal designs using online monitoring. IEEE International Mixed-Signals, Sensors and Systems Test Workshop. 10.1109/ims3tw.2009.5158695
4. Abed, S., Ait Mohamed, O., Al-Sammane, G. An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs. Journal of Computer Science and Technology. 10.1007/s11390-009-9205-8

2008

5. Narayanan, R., Abbasi, N., Zaki, M., Al Sammane, G., Tahar, S. On the simulation performance of contemporary AMS hardware description languages. International Conference on Microelectronics. 10.1109/icm.2008.5393509
6. Abed, S., Ait Mohamed, O., Al Sammane, G. Reachability analysis using multiway decision graphs in the HOL theorem prover. ACM Symposium on Applied Computing. 10.1145/1363686.1363774

2007

7. Dong, Z. J., Zaki, M. H., Al Sammane, G., Tahar, S., Bois, G. Checking properties of PLL designs using run-time verification. International Conference on Microelectronics. 10.1109/icm.2007.4497676
8. Abed, S., Ait Mohamed, O., Yang, Z., Al Sammane, G. Integrating SAT with Multiway Decision Graphs for efficient model checking. International Conference on Microelectronics. 10.1109/icm.2007.4497677
9. Zaki, M. H., Al-Sammane, G., Tahar, S., Bois, G. Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs. Formal Methods in Computer Aided Design (FMCAD). 10.1109/fmcad.2007.4402002 (also recorded as 10.1109/famcad.2007.25)
10. Al Sammane, G., Zaki, M. H., Tahar, S., Bois, G. Constraint-based verification of delta-sigma modulators using interval analysis. IEEE Midwest Symposium on Circuits and Systems. 10.1109/mwscas.2007.4488681
11. Ahmed, A. I., Rahman, S. H., Al-Sammane, G., Ait Mohamed, O. FPGA Emulation environment of different digital carrier synchronizers. IEEE Northeast Workshop on Circuits and Systems. 10.1109/newcas.2007.4487971
12. Dong, Z. J., Zaki, M. H., Al Sammane, G., Tahar, S., Bois, G. Run-time verification using the VHDL-AMS simulation environment. IEEE Northeast Workshop on Circuits and Systems. 10.1109/newcas.2007.4488030
13. Al-Sammane, G., Zaki, M. H., Tahar, S. A Symbolic Methodology for the Verification of Analog and Mixed Signal Designs. Design, Automation and Test in Europe (DATE). 10.1109/date.2007.364599
14. Zaki, M. H., Al-Sammane, G., Tahar, S. Formal Verification of Analog and Mixed Signal Designs in Mathematica. Lecture Notes in Computer Science, Springer. 10.1007/978-3-540-72586-2_37

2004

15. Al Sammane, G., Schmaltz, J., Toma, D., Ostier, P., Borrione, D. TheoSim. ACM International Symposium on Integrated Circuits and System Design. 10.1145/1016568.1016591
16. Al Sammane, G., Schmaltz, J., Borrione, D. Formal design and verification of on chip networking. International Conference on Information and Communication Technologies. 10.1109/ictta.2004.1307937

2002

17. Sylvestre, A., Al Sammane, G., Gattelet, J. Développement de charges d’espace dans des silicones soumis à des forts champs continus. Revue internationale de génie électrique. 10.3166/rige.5.241-252

The eighteenth ORCID entry is the second DOI record of the FMCAD paper (item 9).

Works listed on DBLP but not yet on ORCID

DBLP records five more conference papers under the same name. They are the Grenoble-era work that led to TheoSim and the follow-ups on assertion-based verification:

18. Al Sammane, G., Toma, D., Schmaltz, J., Ostier, P., Borrione, D. Constrained Symbolic Simulation with Mathematica and ACL2. CHARME 2003.
19. Toma, D., Borrione, D., Al Sammane, G. Combining Several Paradigms for Circuit Validation and Verification. CASSIS 2004.
20. Al Sammane, G., Borrione, D., Chevallier, R. Verification of behavioral descriptions by combining symbolic simulation and automatic reasoning. ACM Great Lakes Symposium on VLSI, 2005.
21. Al Sammane, G., Zaki, M. H., Dong, Z. J., Tahar, S. Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL. Forum on Specification and Design Languages (FDL), 2007.
22. Abed, S., Ait Mohamed, O., Al Sammane, G. The Performance of Combining Multiway Decision Graphs and HOL Theorem Prover. FDL 2008.

A note on names

Ghiath Al Sammane and Sam Sammane are the same person. “Sam” is the name I have used professionally in the United States since founding TheoSym and QGI; the publications, the doctorate and the ORCID record carry the legal name. If you are citing the research, use the name on the paper. If you are citing the company work, either is correct.