FairSquare: probabilistic verification of program fairness
Open accessAbstract
With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate fairness and bias in decision-making programs. First, we show that a number of recently proposed formal definitions of fairness can be encoded as probabilistic program properties. Second, with the goal of enabling rigorous reasoning about fairness, we design a novel technique for verifying probabilistic properties that admits a wide class of decision-making programs. Third, we present FairSquare, the first verification tool for automatically certifying that a program meets a given fairness property. We evaluate FairSquare on a range of decision-making programs. Our evaluation demonstrates FairSquare’s ability to verify fairness for a range of different programs, which we show are out-of-reach for state-of-the-art program analysis techniques.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
These evaluation approaches present fairness as a dichotomous outcome: a model is fair, or it isn't, as opposed to quantifying how (un)fair a model is.
“Similar to other evaluation approaches (e.g.[10]), these approaches present fairness as a dichotomous outcome: a model is fair, or it isn't, as opposed to quantifying how (un)fair a model is.”
From Fairness in machine learning: A survey (2024) · cites this paper as [10]
ML Fairness Gym is part of Google's Open AI project, a simulation toolkit to study long-run impacts of ML decisions, and analyzes how algorithms that take fairness into consideration change the underlying data (previous classifications) over time.
“ML Fairness Gym Part of Google's Open AI project, a simulation toolkit to study long-run impacts of ML decisions.5 Analyzes how algorithms that take fairness into consideration change the underlying data (previous classiications) over time (see e.g.[4,5,8,10,12]).”
From Fairness in machine learning: A survey (2024) · cites this paper as [10]
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
The WEKA data mining software: an update
Hall, M., Frank, E., Holmes, G., Pfahringer, B., Reutemann, P., & Witten, I. H. (2009) · ACM SIGKDD Explorations Newsletter · doi:10.1145/1656274.1656278 · Cited by 17,750 · see citing works
(2010) · International Conference on Machine Learning · Cited by 13,995 · see citing works
de Moura, L., & Bjørner, N. (2008) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-78800-3_24 · Cited by 6,595 · see citing works
(2009) · Cited by 6,153 · see citing works
Dwork, C. (2006) · Lecture notes in computer science · doi:10.1007/11787006_1 · Cited by 5,945 · see citing works
Understanding the Metropolis-Hastings Algorithm
Chib, S., & Greenberg, E. (1995) · The American Statistician · doi:10.1080/00031305.1995.10476177 · Cited by 3,745 · see citing works
Dwork, C., Hardt, M., Pitassi, T., Reingold, O., & Zemel, R. (2012) · Proceedings of the 3rd Innovations in Theoretical Computer Science Conference · doi:10.1145/2090236.2090255 · Cited by 3,501 · see citing works
Barocas, S., & Selbst, A. D. (2014) · doi:10.2139/ssrn.2477899 · Cited by 3,048 · see citing works
Equality of Opportunity in Supervised Learning
Hardt, M., Price, E., & Srebro, N. (2016) · arXiv · doi:10.48550/arxiv.1610.02413 · Cited by 2,536 · see citing works
Efficiently computing static single assignment form and the control dependence graph
Cytron, R. K., Jeanne Ferrante, Y., Rosen, B. K., Wegman, M. N., & Zadeck, F. K. (1991) · ACM Transactions on Programming Languages and Systems · doi:10.1145/115372.115320 · Cited by 2,269 · see citing works
Certifying and Removing Disparate Impact
Feldman, M., Friedler, S. A., Moeller, J., Scheidegger, C., & Venkatasubramanian, S. (2015) · Proceedings of the 21th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining · doi:10.1145/2783258.2783311 · Cited by 1,827 · see citing works
Proceedings of the 29th International Conference on Machine Learning (ICML-12)Preprint
Langford, J. C., & Pineau, J. (2012) · arXiv (Cornell University) · doi:10.48550/arxiv.1207.4676 · Cited by 1,687 · see citing works
A Tool for Checking ANSI-C Programs
Clarke, E., Kroening, D., & Lerda, F. (2004) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-24730-2_15 · Cited by 1,408 · see citing works
(2013) · Cited by 1,126 · see citing works
Inherent trade-offs in the fair determination of risk scores
Kleinberg, J., Mullainathan, S., & Raghavan, M. (2017) · Schloss Dagstuhl – Leibniz-Zentrum für Informatik · doi:10.4230/lipics.itcs.2017.43 · Cited by 943 · cited 2× · see citing works
“Nonetheless, the rise of automated decisionmaking has prompted the introduction of a number of formal definitions of fairness, and their utility within different contexts is being actively studied and contested [Dwork et al. 2012; Feldman et al. 2015; Friedler et al. 2016; Hardt et al. 2016; Kleinberg et al. 2017; Rug…”
BackgroundDiscrimination in online ad delivery
Sweeney, L. (2013) · Communications of the ACM · doi:10.1145/2447976.2447990 · Cited by 783 · see citing works
Three naive Bayes approaches for discrimination-free classification.
Calders, T., & Verwer, S. (2010) · Data Mining and Knowledge Discovery · doi:10.1007/s10618-010-0190-x · Cited by 764 · see citing works
Predictive Policing: The Role of Crime Forecasting in Law Enforcement Operations
Perry, W., McInnis, B., Price, C., Smith, S., & Hollywood, J. (2013) · doi:10.7249/rr233 · Cited by 693 · see citing works
A random polynomial-time algorithm for approximating the volume of convex bodies
Dyer, M., FRIEZE, A. M., & Kannan, R. (1991) · Journal of the ACM · doi:10.1145/102782.102783 · Cited by 681 · see citing works
Automated Experiments on Ad Privacy Settings: A Tale of Opacity, Choice, and Discrimination
Datta, A., Tschantz, M. C., & Datta, A. (2015) · Proceedings on Privacy Enhancing Technologies · doi:10.1515/popets-2015-0007 · Cited by 676 · see citing works
Discrimination-aware data mining
Pedreshi, D., Ruggieri, S., & Turini, F. (2008) · Proceedings of the 14th ACM SIGKDD international conference on Knowledge discovery and data mining · doi:10.1145/1401890.1401959 · Cited by 676 · see citing works
Church: a language for generative models
Goodman, N., Mansinghka, V., Roy, D. M., Bonawitz, K., & Tenenbaum, J. B. (2012) · arXiv · doi:10.48550/arxiv.1206.3255 · Cited by 577 · see citing works
Semantics of probabilistic programs
Kozen, D. C. (1981) · Journal of Computer and System Sciences · doi:10.1016/0022-0000(81)90036-2 · Cited by 505 · see citing works
Sweeney, L. (2013) · Queue · doi:10.1145/2460276.2460278 · Cited by 477 · see citing works
Gordon, A. D., Henzinger, T. A., Nori, A. V., & Rajamani, S. K. (2014) · Future of Software Engineering (FOSE) · doi:10.1145/2593882.2593900 · Cited by 372 · see citing works
Self-citationApproximate Reachability Analysis of Piecewise-Linear Dynamical Systems
Eugene Asarin, A., Olivier Bournez, A., Dang, T., & Maler, O. (2000) · Lecture notes in computer science · doi:10.1007/3-540-46430-1_6 · Cited by 343 · see citing works
On the Complexity of Computing the Volume of a Polyhedron
Dyer, M., & FRIEZE, A. M. (1988) · SIAM Journal on Computing · doi:10.1137/0217060 · Cited by 314 · see citing works
Brown, C. W. (2003) · ACM SIGSAM Bulletin · doi:10.1145/968708.968710 · Cited by 296 · see citing works
Libkin, L. O. (2015) · National Conference on Artificial Intelligence · Cited by 273 · see citing works
Measuring Neural Net Robustness with ConstraintsPreprint
Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., & Criminisi, A. (2016) · arXiv (Cornell University) · doi:10.17863/cam.26484 · Cited by 257 · see citing works
Self-citationOn the (im)possibility of fairness
Friedler, S. A., Scheidegger, C., & Venkatasubramanian, S. (2016) · arXiv · doi:10.48550/arxiv.1609.07236 · Cited by 247 · see citing works
Verifying quantitative reliability for programs that execute on unreliable hardware
Carbin, M., Misailovíc, S., & Rinard, M. (2013) · Conference on Object-Oriented Programming Systems, Languages, and Applications · doi:10.1145/2509136.2509546 · Cited by 231 · see citing works
Secure information flow by self-composition
Barthe, G., D’Argenio, P. R., & Rezk, T. (2004) · doi:10.1109/csfw.2004.17 · Cited by 217 · see citing works
Weakest-precondition of unstructured programs
Barnett, M., & Leino, K. R. M. (2005) · ACM SIGSOFT Software Engineering Notes · doi:10.1145/1108768.1108813 · Cited by 203 · see citing works
Secure information flow by self-composition
Barthe, G., D’Argenio, P. R., & Rezk, T. (2004) · IEEE Computer Security Foundations Workshop (CSFW) · doi:10.1109/csfw.2004.1310735 · Cited by 183 · see citing works
Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)
Basu, S., Pollack, R. M., & Roy, M.-F. (2006) · Springer eBooks · Cited by 179 · see citing works
PSI: Exact Symbolic Inference for Probabilistic Programs
Gehr, T., Misailovíc, S., & Vechev, M. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-41528-4_4 · Cited by 161 · see citing works
Geometric Random Walks: A Survey
Vempala, S. (2005) · doi:10.1017/9781009701259.033 · Cited by 150 · see citing works
Probabilistic symbolic execution
Geldenhuys, J., Dwyer, M. B., & Visser, W. (2012) · International Symposium on Software Testing and Analysis · doi:10.1145/2338965.2336773 · Cited by 146 · see citing works
Chaudhuri, S., Gulwani, S., Lublinerman, R., & Navidpour, S. M. (2011) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/2025113.2025131 · Cited by 136 · see citing works
Proceedings for 36th IEEE Symposium on Security and Privacy
Rashidi, Y., & Vaniea, K. E. (2015) · Cited by 129 · see citing works
Inherent Trade-Offs in Algorithmic Fairness
Kleinberg, J. (2018) · Abstracts of the 2018 ACM International Conference on Measurement and Modeling of Computer Systems · doi:10.1145/3219617.3219634 · Cited by 125 · see citing works
Static analysis for probabilistic programs
Sankaranarayanan, S., Chakarov, A., & Gulwani, S. (2013) · Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/2491956.2462179 · Cited by 123 · see citing works
The Paradox of Automation as Anti-Bias Intervention
Ajunwa, I. (2016) · doi:10.2139/ssrn.2746078 · Cited by 122 · see citing works
Weakest-precondition of unstructured programs
Barnett, M., & Leino, K. R. M. (2005) · ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE) · doi:10.1145/1108792.1108813 · Cited by 120 · see citing works
UAI '00: Proceedings of the 16th Conference in Uncertainty in Artificial Intelligence
Storkey, A. (2000) · Cited by 117 · see citing works
Abstract Interpretation of Probabilistic Semantics
Monniaux, D. P. (2000) · Lecture notes in computer science · doi:10.1007/978-3-540-45099-3_17 · Cited by 108 · see citing works
Orthogonal Polyhedra: Representation and Computation
Bournez, O., Maler, O., & Pnueli, A. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48983-5_8 · Cited by 98 · see citing works
An FDA for AlgorithmsPreprint
Tutt, A. (2016) · SSRN Electronic Journal · doi:10.2139/ssrn.2747994 · Cited by 93 · see citing works
Expressing and verifying probabilistic assertions
Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K. S., Grossman, D., & Ceze, L. (2014) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/2594291.2594294 · Cited by 89 · see citing works
Understanding Discrimination in the Scored SocietyPreprint
Zarsky, T. (2014) · SSRN Electronic Journal · Cited by 81 · see citing works
Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence (UAI-15)
Albrecht, S. V., & Ramamoorthy, R. (2015) · Cited by 67 · see citing works
Jovanović, D., & de Moura, L. (2013) · ACM communications in computer algebra · doi:10.1145/2429135.2429155 · Cited by 66 · see citing works
Bayesian inference using data flow analysis
Claret, G., Rajamani, S. K., Nori, A. V., Gordon, A. D., & Borgström, J. (2013) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/2491411.2491423 · Cited by 65 · see citing works
Self-citationProbabilistic inference in hybrid domains by weighted model integration
Belle, V., Passerini, A., & den Broeck, G. V. (2015) · Institutional Research Information System (Università degli Studi di Trento) · Cited by 64 · see citing works
Proving Differential Privacy in Hoare Logic
Barthe, G., Gaboardi, M., Arias, E. J. G., Hsu, J., Kunz, C., & Strub, P.-Y. (2014) · IEEE Computer Security Foundations Workshop (CSFW) · doi:10.1109/csf.2014.36 · Cited by 64 · see citing works
Approximate Counting in SMT and Value Estimation for Probabilistic Programs
Chistikov, D. V., Dimitrova, R., & Majumdar, R. (2015) · Lecture notes in computer science · doi:10.1007/978-3-662-46681-0_26 · Cited by 55 · see citing works
Complexity of Polytope Volume Computation
Khachiyan, L. (1993) · Algorithms and combinatorics · doi:10.1007/978-3-642-58043-7_5 · Cited by 54 · see citing works
Bridging boolean and quantitative synthesis using smoothed proof search
Chaudhuri, S., Clochard, M., & Solar-Lezama, A. (2014) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/2535838.2535859 · Cited by 44 · see citing works
Dynamic Enforcement of Knowledge-Based Security Policies
Mardziel, P., Magill, S., Hicks, M., & Srivatsa, M. (2011) · IEEE Computer Security Foundations Workshop (CSFW) · doi:10.1109/csf.2011.15 · Cited by 44 · see citing works
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
Monniaux, D. P. (2001) · Cited by 44 · see citing works
Algorithmic Transparency via Quantitative Input Influence
Datta, A., Sen, S., & Zick, Y. (2017) · Studies in big data · doi:10.1007/978-3-319-54024-5_4 · Cited by 43 · see citing works
Hashing-based approximate probabilistic inference in hybrid domains
Belle, V., den Broeck, G. V., & Passerini, A. (2015) · Lirias · doi:10.5555/3020847.3020863 · Cited by 39 · see citing works
Hiring by Algorithm: Predicting and Preventing Disparate ImpactPreprint
Ajunwa, I., Friedler, S. A., Scheidegger, C., & Venkatasubramanian, S. (2016) · SSRN Electronic Journal · Cited by 33 · see citing works
Expressing and verifying probabilistic assertions
Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K. S., Grossman, D., & Ceze, L. (2014) · ACM SIGPLAN Notices · doi:10.1145/2666356.2594294 · Cited by 32 · see citing works
An abstract Monte-Carlo method for the analysis of probabilistic programs
Monniaux, D. (2001) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/360204.360211 · Cited by 28 · see citing works
Backwards Abstract Interpretation of Probabilistic Programs
Monniaux, D. P. (2001) · Lecture notes in computer science · doi:10.1007/3-540-45309-1_24 · Cited by 27 · see citing works
Software for exact integration of polynomials over polyhedra
Loera, J. A. D., Dutra, B., Köppe, M., Moreinis, S., Pinto, G., & Wu, J. (2012) · ACM communications in computer algebra · doi:10.1145/2110170.2110175 · Cited by 23 · see citing works
Component Caching in Hybrid Domains with Piecewise Polynomial Densities
Belle, V., den Broeck, G. V., & Passerini, A. (2016) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v30i1.10441 · Cited by 20 · see citing works
Using t-closeness anonymity to control for non-discrimination
Ruggieri, S. (2015) · CINECA IRIS Institutial research information system (University of Pisa) · Cited by 19 · see citing works
Repairing Decision-Making Programs Under Uncertainty
Albarghouthi, A., D’Antoni, L., & Drews, S. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63387-9_9 · Cited by 19 · see citing works
Self-citationUsing t-closeness anonymity to control for non-discrimination
RuggieriSalvatore (2014) · Transactions on data privacy · doi:10.5555/2870621.2870623 · Cited by 10 · see citing works
Management of Time Requirements in Component-Based Systems
Li, Y., Tan, T. H., & Chećhik, M. (2014) · Lecture notes in computer science · doi:10.1007/978-3-319-06410-9_28 · Cited by 9 · see citing works
Flagged first, then by citations
2 of the 75 references couldn’t be matched to a known paper.
Research works printed but not linked: 3
- Amit Datta, Michael Carl Tschantz, and Anupam Datta. 2015. Automated experiments on Ad privacy settings. Proceedings on Privacy Enhancing Technologies 2015, 1 (2015), 92-112.
- Antonio Filieri, Corina S Păsăreanu, and Willem Visser. 2013. Reliability analysis in symbolic pathfinder. In Proceedings of the 2013 International Conference on Software Engineering. IEEE Press, 622-631.
- John Rawls. 2009. A theory of justice. Harvard university press.
Cited by
Sorted by citations
Fairness in machine learning: A survey
Caton, S., & Haas, C. (2024) · ACM Computing Surveys · doi:10.1145/3616865 · Cited by 646 · see citing works
Brun, Y., & Meliou, A. (2018) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3236024.3264838 · Cited by 138 · see citing works
Fairness in Machine Learning: A Survey
Caton, S., & Haas, C. (2020) · arXiv · doi:10.48550/arxiv.2010.04053 · Cited by 646 · see citing works
Formal Specification for Deep Neural Networks
Seshia, S. A., Desai, A., Dreossi, T., Fremont, D. J., Ghosh, S., Kim, E., Shivakumar, S., Vazquez-Chanlatte, M., & Yue, X. (2018) · Lecture notes in computer science · doi:10.1007/978-3-030-01090-4_2 · Cited by 100 · see citing works
Fairness Testing: A Comprehensive Survey and Analysis of Trends
Chen, Z., Zhang, J. M., Hort, M., Harman, M., & Sarro, F. (2024) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3652155 · Cited by 100 · see citing works
A Review on Human–Machine Trust Evaluation: Human-Centric and Machine-Centric Perspectives
Gebru, B., Zeleke, L., Blankson, D., Nabil, M., Nateghi, S., Homaifar, A., & Tunstel, E. (2022) · IEEE Transactions on Human-Machine Systems · doi:10.1109/thms.2022.3144956 · Cited by 101 · see citing works
Balayn, A., Lofi, C., & Houben, G.-J. (2021) · The VLDB Journal · doi:10.1007/s00778-021-00671-8 · Cited by 98 · see citing works
Themis: automatically testing software for discrimination
Angell, R., Johnson, B., Brun, Y., & Meliou, A. (2018) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3236024.3264590 · Cited by 94 · see citing works
Causality-Based Neural Network Repair
Sun, B.-J., Sun, J., Pham, L. H., & Shi, T. (2022) · International Conference on Software Engineering · doi:10.1145/3510003.3510080 · Cited by 125 · see citing works
Scaling exact inference for discrete probabilistic programs
Holtzen, S., den Broeck, G. V., & Millstein, T. D. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428208 · Cited by 86 · see citing works
Robustness of Neural Networks: A Probabilistic and Practical Approach
Mangal, R., Nori, A. V., & Orso, A. (2019) · IEEE/ACM International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) · doi:10.1109/icse-nier.2019.00032 · Cited by 69 · see citing works
Self-citationPerfectly parallel fairness certification of neural networks
Urban, C., Christakis, M., Wüstholz, V., & Zhang, F. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428253 · Cited by 62 · see citing works
Synthesizing coupling proofs of differential privacy
Albarghouthi, A., & Hsu, J. (2017) · Proceedings of the ACM on Programming Languages · doi:10.1145/3158146 · Cited by 61 · see citing works
Self-citationInformation-Theoretic Testing and Debugging of Fairness Defects in Deep Neural Networks
Monjezi, V., Trivedi, A., Tan, G., & Tizpaz-Niari, S. (2023) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse48619.2023.00136 · Cited by 59 · see citing works
Probabilistic verification of fairness properties via concentration
Bastani, O., Zhang, X., & Solar-Lezama, A. (2019) · Proceedings of the ACM on Programming Languages · doi:10.1145/3360544 · Cited by 57 · see citing works
Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective
Meng, M. H., Bai, G.-D., Teo, S. G., Hou, Z., Xiao, Y., Lin, Y., & Dong, J.-S. (2022) · IEEE Transactions on Dependable and Secure Computing · doi:10.1109/tdsc.2022.3179131 · Cited by 99 · see citing works
Albarghouthi, A., & Vinitsky, S. (2019) · ACM Conference on Fairness, Accountability, and Transparency (FAccT) · doi:10.1145/3287560.3287588 · Cited by 52 · see citing works
Self-citationSPPL: probabilistic programming with fast exact symbolic inference
Saad, F. A., Rinard, M., & Mansinghka, V. K. (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3453483.3454078 · Cited by 42 · see citing works
Fairify: Fairness Verification of Neural Networks
Biswas, S., & Rajan, H. (2022) · International Conference on Software Engineering · doi:10.1109/icse48619.2023.00134 · Cited by 50 · see citing works
ASTRAEA: Grammar-based Fairness Testing
Soremekun, E., Udeshi, S., & Chattopadhyay, S. (2022) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2022.3141758 · Cited by 36 · see citing works
Testing Machine Learning Algorithms for Balanced Data Usage
Sharma, A., & Wehrheim, H. (2019) · IEEE International Conference on Software Testing, Verification and Validation (ICST) · doi:10.1109/icst.2019.00022 · Cited by 32 · see citing works
Towards automated verification of smart contract fairness
Liu, Y., Li, Y., Lin, S., & Zhao, R. (2020) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3368089.3409740 · Cited by 32 · see citing works
Compositional Learning and Verification of Neural Network Controllers
Ivanov, R., Jothimurugan, K., Hsu, S., Vaidya, S., Rajeev Alur, A., & Bastani, O. (2021) · ACM Transactions on Embedded Computing Systems · doi:10.1145/3477023 · Cited by 29 · see citing works
Ensuring Fairness Beyond the Training DataPreprint
Mandal, D., Deng, S., Jana, S., Wing, J. M., & Hsu, D. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2007.06029 · Cited by 27 · see citing works
Justicia: A Stochastic SAT Approach to Formally Verify Fairness
Ghosh, B., Basu, D., & Meel, K. S. (2021) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v35i9.16925 · Cited by 25 · see citing works
Probabilistic Verification of Neural Networks Against Group Fairness
Sun, B., Sun, J., Dai, T., & Zhang, L. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-90870-6_5 · Cited by 24 · see citing works
CertiFair: A Framework for Certified Global Fairness of Neural Networks
Khedr, H., & Shoukry, Y. (2023) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v37i7.25994 · Cited by 19 · see citing works
What algorithmic evaluation fails to deliver: respectful treatment and individualized consideration
Chun, J. S., David De Cremer, A., Oh, E., & Kim, Y. (2024) · Scientific Reports · doi:10.1038/s41598-024-76320-1 · Cited by 19 · see citing works
Guaranteed bounds for posterior inference in universal probabilistic programming
Beutner, R., Ong, C.-H. L., & Zaiser, F. (2022) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3519939.3523721 · Cited by 18 · see citing works
Verifying Fairness in Quantum Machine Learning
Guan, J., Fang, W. S., & Ying, M. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-13188-2_20 · Cited by 18 · see citing works
Symbolic execution for randomized programs
Susag, Z. J., Lahiri, S., Hsu, J., & Roy, S. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3563344 · Cited by 18 · see citing works
Bayonet: probabilistic inference for networks
Gehr, T., Misailovíc, S., Tsankov, P., Vanbever, L., Wiesmann, P., & Vechev, M. (2018) · ACM SIGPLAN Notices · doi:10.1145/3296979.3192400 · Cited by 17 · see citing works
AQUA: Automated Quantized Inference for Probabilistic Programs
Huang, Z., Dutta, S., & Misailovíc, S. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-88885-5_16 · Cited by 17 · see citing works
Bayonet: probabilistic inference for networks
Gehr, T., Misailovíc, S., Tsankov, P., Vanbever, L., Wiesmann, P., & Vechev, M. (2018) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3192366.3192400 · Cited by 16 · see citing works
Trace abstraction modulo probability
Smith, C., Hsu, J., & Albarghouthi, A. (2019) · Proceedings of the ACM on Programming Languages · doi:10.1145/3290352 · Cited by 16 · see citing works
Self-citationIndividual Fairness Guarantees for Neural Networks
Benussi, E., Patanè, A., Wicker, M., Laurenti, L., & Kwiatkowska, M. (2022) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2022/92 · Cited by 14 · see citing works
PSense: Automatic Sensitivity Analysis for Probabilistic Programs
Huang, Z., Wang, Z., & Misailovíc, S. (2018) · Lecture notes in computer science · doi:10.1007/978-3-030-01090-4_23 · Cited by 14 · see citing works
Monitoring Algorithmic Fairness
Henzinger, T. A., Karimi, M., Kueffner, K., & Mallik, K. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-37703-7_17 · Cited by 13 · see citing works
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Randone, F., Bortolussi, L., Incerto, E., & Tribastone, M. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3632905 · Cited by 13 · see citing works
Baluta, T., Shen, S., Shinde, S., Meel, K. S., & Saxena, P. (2019) · Zenodo (CERN European Organization for Nuclear Research) · doi:10.1145/3319535.3354245 · Cited by 90 · see citing works
Constraint-Driven Explanations for Black-Box ML Models
Shrotri, A. A., Narodytska, N., Ignatiev, A., Meel, K. S., Marques-Silva, J. P., & Vardi, M. Y. (2022) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v36i8.20805 · Cited by 11 · see citing works
Algorithmic Fairness Verification with Graphical Models
Ghosh, B., Basu, D., & Meel, K. S. (2022) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v36i9.21187 · Cited by 11 · see citing works
Synthesizing Fair Decision Trees via Iterative Constraint Solving
Wang, J., Li, Y., & Wang, C. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-13188-2_18 · Cited by 11 · see citing works
Online Fairness Auditing through Iterative Refinement
Maneriker, P., Burley, C., & Parthasarathy, S. (2023) · ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD) · doi:10.1145/3580305.3599454 · Cited by 10 · see citing works
Bit Blasting Probabilistic Programs
Garg, P., Holtzen, S., den Broeck, G. V., & Millstein, T. D. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3656412 · Cited by 10 · see citing works
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Thompson, K., Saavedra, N., Carrott, P., Fisher, K. D., Sanchez-Stern, A., Brun, Y., Ferreira, J. F., Lerner, S., & First, E. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00161 · Cited by 14 · see citing works
Continualization of Probabilistic Programs With Correction
Laurel, J., & Misailovíc, S. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-44914-8_14 · Cited by 10 · see citing works
Fair Normalizing FlowsPreprint
Balunović, M., Ruoss, A., & Vechev, M. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2106.05937 · Cited by 10 · see citing works
Latent Space Smoothing for Individually Fair Representations
Peychev, M., Ruoss, A., Balunović, M., Baader, M., & Vechev, M. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-19778-9_31 · Cited by 9 · see citing works
PRoofster: Automated Formal Verification
Agrawal, A., First, E., Kaufman, Z., Reichel, T., Zhang, S., Zhou, T., Sanchez-Stern, A., Ringer, T., & Brun, Y. (2023) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse-companion58688.2023.00018 · Cited by 9 · see citing works
Certifying the Fairness of KNN in the Presence of Dataset Bias
Li, Y., Wang, J., & Wang, C. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-37703-7_16 · Cited by 8 · see citing works
Enhancing SMT-based Weighted Model Integration by structure awareness
Spallitta, G., Masina, G., Morettin, P., Passerini, A., & Sebastiani, R. (2024) · Artificial Intelligence · doi:10.1016/j.artint.2024.104067 · Cited by 8 · see citing works
Fairquant: Certifying and Quantifying Fairness of Deep Neural Networks
Kim, B. H., Wang, J., & Wang, C. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00016 · Cited by 10 · see citing works
DeepGemini: Verifying Dependency Fairness for Deep Neural Network
Xie, X., Zhang, F.-Y., Hu, X., & Ma, L. (2023) · AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v37i12.26779 · Cited by 9 · see citing works
Static Analysis of Data Science Software
Urban, C. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-32304-2_2 · Cited by 8 · see citing works
Certifying Fairness of Probabilistic Circuits
Selvam, N. R., den Broeck, G. V., & Choi, Y. (2023) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v37i10.26447 · Cited by 7 · see citing works
Covering All the Bases: Type-Based Verification of Test Input Generators
Zhou, Z., Mishra, A., Delaware, B., & Jagannathan, S. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3591271 · Cited by 7 · see citing works
Probabilistic Lipschitz Analysis of Neural Networks
Mangal, R., Sarangmath, K., Nori, A. V., & Orso, A. (2020) · Sensors Applications Symposium · doi:10.1007/978-3-030-65474-0_13 · Cited by 13 · see citing works
Self-citationGenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
Huot, M., Ghavami, M., Lew, A. K., Schaechtle, U., Freer, C. E., Shelby, Z., Rinard, M., Saad, F. A., & Mansinghka, V. K. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3656409 · Cited by 5 · see citing works
Specifying and Testing k-Safety Properties for Machine-Learning Models
Christakis, M., Enişer, H. F., Hoffmann, J., Singla, A. K., & Wüstholz, V. (2023) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2023/528 · Cited by 5 · see citing works
Gerten, M. C., Lathrop, J. I., Cohen, M. B., & Klinge, T. H. (2020) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3324884.3416638 · Cited by 5 · see citing works
Monitoring Algorithmic Fairness Under Partial Observations
Henzinger, T. A., Kueffner, K., & Mallik, K. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-44267-4_15 · Cited by 4 · see citing works
Stream-Based Monitoring of Algorithmic Fairness
Baumeister, J., Finkbeiner, B., Scheerer, F., Siber, J., & Wagenpfeil, T. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-90643-5_4 · Cited by 4 · see citing works
Hybrid Probabilistic Inference with Logical and Algebraic Constraints: a Survey
Morettin, P., Martires, P. Z. D., Kolb, S., & Passerini, A. (2021) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2021/617 · Cited by 4 · see citing works
The Random Conditional Distribution for Higher-Order Probabilistic InferencePreprint
Tavares, Z., Zhang, X., Minaysan, E., Burroni, J., Ranganath, R., & Solar-Lezama, A. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1903.10556 · Cited by 4 · see citing works
Explainable Global Fairness Verification of Tree-Based Classifiers
Calzavara, S., Cazzaro, L., Lucchese, C., & Marcuzzi, F. (2023) · IEEE Conference on Secure and Trustworthy Machine Learning (SaTML) · doi:10.1109/satml54575.2023.00011 · Cited by 3 · see citing works
FETA: Fairness Enforced Verifying, Training, and Predicting Algorithms for Neural Networks
Mohammadi, K., Sivaraman, A., & Farnadi, G. (2023) · ACM Conference on Equity and Access in Algorithms, Mechanisms, and Optimization (EAAMO) · doi:10.1145/3617694.3623243 · Cited by 3 · see citing works
An Information-Flow Perspective on Algorithmic Fairness
Teuber, S., & Beckert, B. (2024) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v38i14.29458 · Cited by 2 · see citing works
Checking trustworthiness of probabilistic computations in a typed natural deduction system
D’Asaro, F. A., Genco, F. A., & Primiero, G. (2025) · Journal of Logic and Computation · doi:10.1093/logcom/exaf003 · Cited by 3 · see citing works
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Sanchez-Stern, A., Varghese, A., Kaufman, Z., Zhang, D., Ringer, T., & Brun, Y. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00033 · Cited by 4 · see citing works
Probabilistic Symbolic Analysis of Neural Networks
Converse, H., Filieri, A., Gopinath, D., & Păsăreanu, C. S. (2020) · Proceedings/Proceedings - International Symposium on Software Reliability Engineering · doi:10.1109/issre5003.2020.00023 · Cited by 3 · see citing works
Batz, K., Katoen, J.-P., Randone, F., & Winkler, T. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720429 · Cited by 2 · see citing works
FairSense: Long-Term Fairness Analysis of ML-Enabled Systems
She, Y., Biswas, S., Kästner, C., & Kang, E. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00159 · Cited by 2 · see citing works
Towards Systematic Specification and Verification of Fairness Requirements: A Position Paper
Ramadan, Q., Ruohonen, J., Tiwari, A., Alami, A., & Boukhers, Z. (2025) · IEEE International Requirements Engineering Conference Workshops (REW) · doi:10.1109/rew66121.2025.00059 · Cited by 2 · see citing works
Automated quantized inference for probabilistic programs with AQUA
Huang, Z., Dutta, S., & Misailovíc, S. (2022) · Innovations in Systems and Software Engineering · doi:10.1007/s11334-021-00433-3 · Cited by 2 · see citing works
FairNNV: The Neural Network Verification Tool For Certifying Fairness
Tumlin, A. M., Lopez, D. M., Robinette, P. K., Zhao, Y., Derr, T., & Johnson, T. T. (2024) · ACM International Conference on AI in Finance (ICAIF) · doi:10.1145/3677052.3698677 · Cited by 2 · see citing works
Logic + probabilistic programming + causal laws
Belle, V. (2023) · Royal Society Open Science · doi:10.1098/rsos.230785 · Cited by 2 · see citing works
Program Analysis for Adaptive Data Analysis
Liu, J., Qu, W., Gaboardi, M., Garg, D., & Ullman, J. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3656414 · Cited by 2 · see citing works
Probabilistic Verification of Fairness Properties via ConcentrationPreprint
Bastani, O., Zhang, X., & Solar-Lezama, A. (2018) · arXiv (Cornell University) · doi:10.48550/arxiv.1812.02573 · Cited by 2 · see citing works
The Fair Game: Auditing & debiasing AI algorithms over time
Basu, D., & Das, U. (2025) · Cambridge Forum on AI Law and Governance · doi:10.1017/cfl.2025.8 · Cited by 1 · see citing works
MBFair: a model-based verification methodology for detecting violations of individual fairness
Ramadan, Q., Konersmann, M., Ahmadian, A. S., Jürjens, J., & Staab, S. (2024) · Software & Systems Modeling · doi:10.1007/s10270-024-01184-y · Cited by 1 · see citing works
Language-Based Security for Low-Level MPC
Skalka, C., & Near, J. P. (2024) · International Symposium on Principles and Practice of Declarative Programming (PPDP) · doi:10.1145/3678232.3678246 · Cited by 1 · see citing works
Checking δ-Satisfiability of Reals with Integrals
Rivera, C., Bhusal, B., Chadha, R., Sistla, A. P., & Viswanathan, M. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720446 · Cited by 1 · see citing works
Algorithmic Fairness: A Runtime Perspective
Cano, F., Henzinger, T. A., & Kueffner, K. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-05435-7_1 · Cited by 1 · see citing works
Correct-by-Construction: Certified Individual Fairness through Neural Network Training
Zhang, R.-H., & Sun, J. (2025) · Proc. ACM Program. Lang. · doi:10.1145/3763107 · Cited by 2 · see citing works
Fairness-guided SMT-based Rectification of Decision Trees and Random ForestsPreprint
Zhang, J., Beschastnikh, I., Mechtaev, S., & Roychoudhury, A. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2011.11001 · Cited by 1 · see citing works
Fairness: A Formal-Methods Perspective
Albarghouthi, A. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-99725-4_1
Self-citationExact Symbolic Inference in Probabilistic Programs via Sum-Product Representations.Preprint
Saad, F. A., Rinard, M., & Mansinghka, V. K. (2020) · arXiv (Cornell University)
Synthesizing Machine Learning Programs with PAC Guarantees via Statistical SketchingPreprint
Bastani, O. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2110.05390
Khan, S., Chatterjee, B., & Pande, S. (2022) · International Conference on Supercomputing · doi:10.1145/3524059.3532393
On Retrofitting Provenance for Transparent and Fair Software - Drivers and Challenges
Dietrich, J. B., Galster, M., & Luczak–Roesch, M. (2023) · doi:10.1109/fairware59297.2023.00007
Uncovering Discrimination Clusters: Quantifying and Explaining Systematic Fairness Violations
Akash, R. D., Kumar, A., Monjezi, V., Trivedi, A., Tan, G., & Tizpaz-Niari, S. (2025) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1109/ase63991.2025.00141
ProofCoop: Collaborative Automated Formal Verification
Kaufman, Z., First, E., Sanchez-Stern, A., Thompson, K., Lerner, S., & Brun, Y. (2026) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3744916.3787783
- Authors
- Albarghouthi, A., D'Antoni, L., Drews, S., & Nori, A. V.
- Affiliations
- University of Wisconsin–Madison (US)
- University of Wisconsin-Madison, USA
- Microsoft Research (United Kingdom) (GB)
- Venue
- Proceedings of the ACM on Programming Languages
- Published
- 2017-10-12
- Volume
- 1
- Issue
- OOPSLA
- Pages
- 1-30
- ISSN
- 2475-1421 (ISSN-L)
- OpenAlex
- W2762833920
- Cited by
- 94
- References
- 75
- Citations by year
- 2026: 1 · 2025: 13 · 2024: 11 · 2023: 18 · 2022: 14 · 2021: 9 · 2020: 10 · 2019: 9 · 2018: 8 · 2017: 1
- FWCI
- 4.57
- Type
- journal article
- Language
- en
- Open access
- bronze
- doi.org
- Locations
- Proceedings of the ACM on Programming Languages (publishedVersion)
- Funders
- NSF (1704117 and 1566015)
- Topics
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Keywords
- probabilistic verification, algorithmic fairness, automated verification tools, algorithmic bias
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
